| 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 3065 | . 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑 |
| 3 | 2 | rgenw 3065 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: porpss 7747 fnmpoi 8095 mptmpoopabbrd 8105 relmpoopab 8119 cantnfvalf 9705 ixxf 13397 fzf 13551 fzof 13696 rexfiuz 15386 sadcf 16490 prdsvallem 17499 prdsds 17509 homfeq 17737 comfeq 17749 wunnat 18004 eldmcoa 18110 catcfuccl 18163 relxpchom 18226 catcxpccl 18252 plusffval 18659 grpsubfval 19001 lsmass 19687 efgval2 19742 dmdprd 20018 dprdval 20023 scaffval 20878 ipffval 21666 psdmul 22170 eltx 23576 xkotf 23593 txcnp 23628 txcnmpt 23632 txrest 23639 txlm 23656 txflf 24014 dscmet 24585 xrtgioo 24828 ishtpy 25004 opnmblALT 25638 tglnfn 28555 wwlksonvtx 29875 wspthnonp 29879 clwwlknondisj 30130 hlimreui 31258 aciunf1lem 32672 ofoprabco 32674 lsmssass 33430 dya2iocct 34282 icoreresf 37353 curfv 37607 ptrest 37626 poimirlem26 37653 rrnval 37834 atpsubN 39755 clsk3nimkb 44053 2arymaptf1 48574 |
| Copyright terms: Public domain | W3C validator |