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 3147 | . 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑 |
3 | 2 | rgenw 3147 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: porpss 7442 fnmpoi 7757 relmpoopab 7778 cantnfvalf 9116 ixxf 12736 fzf 12884 fzof 13023 rexfiuz 14695 sadcf 15790 prdsval 16716 prdsds 16725 homfeq 16952 comfeq 16964 wunnat 17214 eldmcoa 17313 catcfuccl 17357 relxpchom 17419 catcxpccl 17445 plusffval 17846 grpsubfval 18085 lsmass 18724 efgval2 18779 dmdprd 19049 dprdval 19054 scaffval 19581 ipffval 20720 eltx 22104 xkotf 22121 txcnp 22156 txcnmpt 22160 txrest 22167 txlm 22184 txflf 22542 dscmet 23109 xrtgioo 23341 ishtpy 23503 opnmblALT 24131 tglnfn 26260 wwlksonvtx 27560 wspthnonp 27564 clwwlknondisj 27817 hlimreui 28943 aciunf1lem 30335 ofoprabco 30337 dya2iocct 31437 icoreresf 34515 curfv 34753 ptrest 34772 poimirlem26 34799 rrnval 34986 atpsubN 36769 clsk3nimkb 40268 |
Copyright terms: Public domain | W3C validator |