![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexlimivv | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
Ref | Expression |
---|---|
rexlimivv.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
rexlimivv | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivv.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) | |
2 | 1 | rexlimdva 3153 | . 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | rexlimiv 3146 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∃wrex 3074 |
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-ex 1783 df-rex 3075 |
This theorem is referenced by: r19.29vva 3208 2reu5 3721 2reu4 4489 opelxp 5674 elinxp 5980 reuop 6250 opiota 7996 f1o2ndf1 8059 poseq 8095 soseq 8096 tfrlem5 8331 xpdom2 9018 1sdomOLD 9200 unxpdomlem3 9203 unfiOLD 9264 elfiun 9373 ttrcltr 9659 xpnum 9894 kmlem9 10101 nqereu 10872 distrlem5pr 10970 mulid1 11160 1re 11162 mul02 11340 cnegex 11343 recex 11794 creur 12154 creui 12155 cju 12156 elz2 12524 zaddcl 12550 qre 12885 qaddcl 12897 qnegcl 12898 qmulcl 12899 qreccl 12901 elpqb 12908 hash2prd 14381 elss2prb 14393 fundmge2nop0 14398 wrdl3s3 14858 replim 15008 prodmo 15826 odd2np1 16230 opoe 16252 omoe 16253 opeo 16254 omeo 16255 qredeu 16541 pythagtriplem1 16695 pcz 16760 4sqlem1 16827 4sqlem2 16828 4sqlem4 16831 mul4sq 16833 pmtr3ncom 19264 efgmnvl 19503 efgrelexlema 19538 ring1ne0 20022 txuni2 22932 tx2ndc 23018 blssioo 24174 tgioo 24175 ioorf 24953 ioorinv 24956 ioorcl 24957 dyaddisj 24976 mbfid 25015 elply 25572 vmacl 26483 efvmacl 26485 vmalelog 26569 2sqlem2 26782 mul2sq 26783 2sqlem7 26788 2sqnn0 26802 2sqreultblem 26812 pntibnd 26957 ostth 27003 scutf 27173 legval 27568 upgredgpr 28135 nbgr2vtx1edg 28340 cusgredg 28414 usgredgsscusgredg 28449 wwlksnwwlksnon 28902 n4cyclfrgr 29277 vdgn1frgrv2 29282 friendshipgt3 29384 lpni 29464 nsnlplig 29465 nsnlpligALT 29466 n0lpligALT 29468 ipasslem5 29819 ipasslem11 29824 hhssnv 30248 shscli 30301 shsleji 30354 shsidmi 30368 spansncvi 30636 superpos 31338 chirredi 31378 mdsymlem6 31392 rnmposs 31632 1fldgenq 32129 ccfldextdgrr 32396 cnre2csqima 32532 dya2icobrsiga 32916 dya2iocnrect 32921 dya2iocucvr 32924 sxbrsigalem2 32926 afsval 33324 satfv0 33992 satfrnmapom 34004 satfv0fun 34005 satf00 34008 sat1el2xp 34013 fmla0xp 34017 fmla1 34021 msubco 34165 elaltxp 34589 altxpsspw 34591 funtransport 34645 funray 34754 funline 34756 ellines 34766 linethru 34767 icoreresf 35852 icoreclin 35857 relowlssretop 35863 relowlpssretop 35864 itg2addnc 36161 isline 38231 sn-it0e0 40913 sn-mulid2 40933 sn-0tie0 40937 sn-mul02 40938 mzpcompact2lem 41103 sprvalpw 45746 sprvalpwn0 45749 prsprel 45753 prpair 45767 prprvalpw 45781 reuopreuprim 45792 nnsum3primesgbe 46058 nnsum4primesodd 46062 nnsum4primesoddALTV 46063 tgblthelfgott 46081 nnpw2pb 46747 2arymaptf1 46813 |
Copyright terms: Public domain | W3C validator |