![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rgen2w | Structured version Visualization version GIF version |
Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rgenw.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
rgen2w | ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rgenw.1 | . . 3 ⊢ 𝜑 | |
2 | 1 | rgenw 2953 | . 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑 |
3 | 2 | rgenw 2953 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 |
This theorem depends on definitions: df-bi 197 df-ral 2946 |
This theorem is referenced by: porpss 6983 fnmpt2i 7284 relmpt2opab 7304 cantnfvalf 8600 ixxf 12223 fzf 12368 fzof 12506 rexfiuz 14131 sadcf 15222 prdsval 16162 prdsds 16171 homfeq 16401 comfeq 16413 wunnat 16663 eldmcoa 16762 catcfuccl 16806 relxpchom 16868 catcxpccl 16894 plusffval 17294 lsmass 18129 efgval2 18183 dmdprd 18443 dprdval 18448 scaffval 18929 ipffval 20041 eltx 21419 xkotf 21436 txcnp 21471 txcnmpt 21475 txrest 21482 txlm 21499 txflf 21857 dscmet 22424 xrtgioo 22656 ishtpy 22818 opnmblALT 23417 tglnfn 25487 wwlksonvtx 26805 wspthnonp 26813 clwwlknondisj 27086 clwwlknondisjOLD 27090 hlimreui 28224 aciunf1lem 29590 ofoprabco 29592 dya2iocct 30470 icoreresf 33330 curfv 33519 ptrest 33538 poimirlem26 33565 rrnval 33756 atpsubN 35357 clsk3nimkb 38655 |
Copyright terms: Public domain | W3C validator |