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 3150 | . 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑 |
3 | 2 | rgenw 3150 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wral 3138 |
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 3143 |
This theorem is referenced by: porpss 7442 fnmpoi 7759 relmpoopab 7780 cantnfvalf 9117 ixxf 12738 fzf 12886 fzof 13025 rexfiuz 14697 sadcf 15792 prdsval 16718 prdsds 16727 homfeq 16954 comfeq 16966 wunnat 17216 eldmcoa 17315 catcfuccl 17359 relxpchom 17421 catcxpccl 17447 plusffval 17848 grpsubfval 18087 lsmass 18726 efgval2 18781 dmdprd 19051 dprdval 19056 scaffval 19583 ipffval 20722 eltx 22106 xkotf 22123 txcnp 22158 txcnmpt 22162 txrest 22169 txlm 22186 txflf 22544 dscmet 23111 xrtgioo 23343 ishtpy 23505 opnmblALT 24133 tglnfn 26261 wwlksonvtx 27561 wspthnonp 27565 clwwlknondisj 27818 hlimreui 28944 aciunf1lem 30336 ofoprabco 30338 dya2iocct 31438 icoreresf 34516 curfv 34754 ptrest 34773 poimirlem26 34800 rrnval 34988 atpsubN 36771 clsk3nimkb 40270 |
Copyright terms: Public domain | W3C validator |