![]() |
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 3145 | . 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | rexlimiv 3138 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2099 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-rex 3061 |
This theorem is referenced by: r19.29vva 3204 2reu5 3752 2reu4 4531 opelxp 5718 elinxp 6028 reuop 6304 opiota 8073 f1o2ndf1 8136 poseq 8172 soseq 8173 tfrlem5 8410 xpdom2 9105 1sdomOLD 9283 unxpdomlem3 9286 unfiOLD 9347 elfiun 9473 ttrcltr 9759 xpnum 9994 kmlem9 10201 nqereu 10972 distrlem5pr 11070 mulrid 11262 1re 11264 mul02 11442 cnegex 11445 recex 11896 creur 12258 creui 12259 cju 12260 elz2 12628 zaddcl 12654 qre 12989 qaddcl 13001 qnegcl 13002 qmulcl 13003 qreccl 13005 elpqb 13012 hash2prd 14494 elss2prb 14506 fundmge2nop0 14511 wrdl3s3 14971 replim 15121 prodmo 15938 odd2np1 16343 opoe 16365 omoe 16366 opeo 16367 omeo 16368 qredeu 16659 pythagtriplem1 16818 pcz 16883 4sqlem1 16950 4sqlem2 16951 4sqlem4 16954 mul4sq 16956 pmtr3ncom 19473 efgmnvl 19712 efgrelexlema 19747 ring1ne0 20278 pzriprnglem8 21478 txuni2 23560 tx2ndc 23646 blssioo 24802 tgioo 24803 ioorf 25593 ioorinv 25596 ioorcl 25597 dyaddisj 25616 mbfid 25655 elply 26222 vmacl 27146 efvmacl 27148 vmalelog 27234 2sqlem2 27447 mul2sq 27448 2sqlem7 27453 2sqnn0 27467 2sqreultblem 27477 pntibnd 27622 ostth 27668 scutf 27842 elzn0s 28342 remulscllem1 28351 legval 28511 upgredgpr 29078 nbgr2vtx1edg 29286 cusgredg 29360 usgredgsscusgredg 29396 wwlksnwwlksnon 29849 n4cyclfrgr 30224 vdgn1frgrv2 30229 friendshipgt3 30331 lpni 30413 nsnlplig 30414 nsnlpligALT 30415 n0lpligALT 30417 ipasslem5 30768 ipasslem11 30773 hhssnv 31197 shscli 31250 shsleji 31303 shsidmi 31317 spansncvi 31585 superpos 32287 chirredi 32327 mdsymlem6 32341 rnmposs 32591 1fldgenq 33172 ccfldextdgrr 33558 cnre2csqima 33726 dya2icobrsiga 34110 dya2iocnrect 34115 dya2iocucvr 34118 sxbrsigalem2 34120 afsval 34517 satfv0 35186 satfrnmapom 35198 satfv0fun 35199 satf00 35202 sat1el2xp 35207 fmla0xp 35211 fmla1 35215 msubco 35359 elaltxp 35799 altxpsspw 35801 funtransport 35855 funray 35964 funline 35966 ellines 35976 linethru 35977 icoreresf 37059 icoreclin 37064 relowlssretop 37070 relowlpssretop 37071 itg2addnc 37375 isline 39438 sn-it0e0 42195 sn-mullid 42215 sn-0tie0 42219 sn-mul02 42220 mzpcompact2lem 42408 sprvalpw 47052 sprvalpwn0 47055 prsprel 47059 prpair 47073 prprvalpw 47087 reuopreuprim 47098 nnsum3primesgbe 47364 nnsum4primesodd 47368 nnsum4primesoddALTV 47369 tgblthelfgott 47387 nnpw2pb 47975 2arymaptf1 48041 |
Copyright terms: Public domain | W3C validator |