![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rgen2 | Structured version Visualization version GIF version |
Description: Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3347 since it depends on a smaller set of axioms. (Contributed by NM, 30-May-1999.) |
Ref | Expression |
---|---|
rgen2.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) |
Ref | Expression |
---|---|
rgen2 | ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rgen2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) | |
2 | 1 | ralrimiva 3144 | . 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑) |
3 | 2 | rgen 3067 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ral 3066 |
This theorem is referenced by: rgen3 3200 invdisjrabw 5095 invdisjrab 5096 sosn 5723 isoid 7279 f1owe 7303 epweon 7714 epweonALT 7715 f1stres 7950 f2ndres 7951 fnwelem 8068 soseq 8096 issmo 8299 oawordeulem 8506 naddf 8632 ecopover 8767 unfilem2 9262 dffi2 9366 inficl 9368 fipwuni 9369 fisn 9370 dffi3 9374 cantnfvalf 9608 r111 9718 alephf1 10028 alephiso 10041 dfac5lem4 10069 kmlem9 10101 ackbij1lem17 10179 fin1a2lem2 10344 fin1a2lem4 10346 axcc2lem 10379 smobeth 10529 nqereu 10872 addpqf 10887 mulpqf 10889 genpdm 10945 axaddf 11088 axmulf 11089 subf 11410 mulnzcnopr 11808 negiso 12142 cnref1o 12917 xaddf 13150 xmulf 13198 ioof 13371 om2uzf1oi 13865 om2uzisoi 13866 wrd2ind 14618 wwlktovf1 14853 reeff1 16009 divalglem9 16290 bitsf1 16333 smupf 16365 gcdf 16399 eucalgf 16466 qredeu 16541 1arith 16806 vdwapf 16851 xpsff1o 17456 catideu 17562 sscres 17713 fpwipodrs 18436 letsr 18489 mgmidmo 18522 frmdplusg 18671 efmndmgm 18702 smndex1mgm 18724 pwmnd 18754 mulgfval 18881 nmznsg 18977 efgmf 19502 efglem 19505 efgred 19537 isabli 19585 brric 20187 xrsmgm 20848 xrs1cmn 20853 xrge0subm 20854 xrsds 20856 cnsubmlem 20861 cnsubrglem 20863 nn0srg 20883 rge0srg 20884 rzgrp 21043 fibas 22343 fctop 22370 cctop 22372 iccordt 22581 txuni2 22932 fsubbas 23234 zfbas 23263 ismeti 23694 dscmet 23944 qtopbaslem 24138 tgqioo 24179 xrsxmet 24188 xrsdsre 24189 retopconn 24208 iccconn 24209 divcn 24247 abscncf 24280 recncf 24281 imcncf 24282 cjcncf 24283 iimulcn 24317 icopnfhmeo 24322 iccpnfhmeo 24324 xrhmeo 24325 cnllycmp 24335 bndth 24337 iundisj2 24929 dyadf 24971 reefiso 25823 recosf1o 25907 cxpcn3 26117 sgmf 26510 2lgslem1b 26756 lrcut 27254 addsf 27314 negscut 27359 negsf1o 27371 tgjustf 27457 ercgrg 27501 2wspmdisj 29323 isabloi 29535 smcnlem 29681 cncph 29803 hvsubf 29999 hhip 30161 hhph 30162 helch 30227 hsn0elch 30232 hhssabloilem 30245 hhshsslem2 30252 shscli 30301 shintcli 30313 pjmf1 30700 idunop 30962 0cnop 30963 0cnfn 30964 idcnop 30965 idhmop 30966 0hmop 30967 adj0 30978 lnophsi 30985 lnopunii 30996 lnophmi 31002 nlelshi 31044 riesz4i 31047 cnlnadjlem6 31056 cnlnadjlem9 31059 adjcoi 31084 bra11 31092 pjhmopi 31130 iundisj2f 31550 iundisj2fi 31742 xrstos 31912 xrge0omnd 31961 reofld 32176 xrge0slmod 32180 iistmd 32523 cnre2csqima 32532 mndpluscn 32547 raddcn 32550 xrge0iifiso 32556 xrge0iifmhm 32560 xrge0pluscn 32561 cnzh 32591 rezh 32592 br2base 32909 sxbrsiga 32930 signswmnd 33209 cardpred 33734 nummin 33735 indispconn 33868 cnllysconn 33879 ioosconn 33881 rellysconn 33885 fmlaomn0 34024 gonan0 34026 goaln0 34027 fneref 34851 dnicn 34984 f1omptsnlem 35836 isbasisrelowl 35858 poimirlem27 36134 mblfinlem1 36144 mblfinlem2 36145 exidu1 36344 rngoideu 36391 isomliN 37730 idlaut 38588 resubf 40879 sn-subf 40926 mzpclall 41079 frmx 41266 frmy 41267 kelac2lem 41420 onsucf1o 41636 ontric3g 41868 clsk1indlem3 42389 icof 43514 natglobalincr 45190 sprsymrelf1 45762 fmtnof1 45801 prmdvdsfmtnof1 45853 uspgrsprf1 46123 plusfreseq 46140 nnsgrpmgm 46184 nnsgrp 46185 nn0mnd 46187 2zrngamgm 46311 2zrngmmgm 46318 2zrngnmrid 46322 ldepslinc 46664 rrx2xpref1o 46878 rrx2plordisom 46883 |
Copyright terms: Public domain | W3C validator |