![]() |
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 3064 | . 2 ⊢ ∀𝑦 ∈ 𝐵 𝜑 |
3 | 2 | rgenw 3064 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wral 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 |
This theorem depends on definitions: df-bi 206 df-ral 3061 |
This theorem is referenced by: porpss 7700 fnmpoi 8038 relmpoopab 8062 cantnfvalf 9642 ixxf 13316 fzf 13470 fzof 13611 rexfiuz 15276 sadcf 16376 prdsvallem 17382 prdsds 17392 homfeq 17620 comfeq 17632 wunnat 17889 wunnatOLD 17890 eldmcoa 17997 catcfuccl 18051 catcfucclOLD 18052 relxpchom 18115 catcxpccl 18141 catcxpcclOLD 18142 plusffval 18549 grpsubfval 18843 lsmass 19501 efgval2 19556 dmdprd 19827 dprdval 19832 scaffval 20439 ipffval 21134 eltx 23001 xkotf 23018 txcnp 23053 txcnmpt 23057 txrest 23064 txlm 23081 txflf 23439 dscmet 24010 xrtgioo 24251 ishtpy 24417 opnmblALT 25049 tglnfn 27663 wwlksonvtx 28974 wspthnonp 28978 clwwlknondisj 29229 hlimreui 30355 aciunf1lem 31756 ofoprabco 31758 lsmssass 32370 dya2iocct 33110 icoreresf 36037 curfv 36272 ptrest 36291 poimirlem26 36318 rrnval 36500 atpsubN 38429 clsk3nimkb 42562 2arymaptf1 46987 |
Copyright terms: Public domain | W3C validator |