| 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 3155 | . 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓)) |
| 3 | 2 | rexlimiv 3148 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: r19.29vva 3216 2reu5 3764 2reu4 4523 opelxp 5721 elinxp 6037 reuop 6313 opiota 8084 f1o2ndf1 8147 poseq 8183 soseq 8184 tfrlem5 8420 xpdom2 9107 1sdomOLD 9285 unxpdomlem3 9288 elfiun 9470 ttrcltr 9756 xpnum 9991 kmlem9 10199 nqereu 10969 distrlem5pr 11067 mulrid 11259 1re 11261 mul02 11439 cnegex 11442 recex 11895 creur 12260 creui 12261 cju 12262 elz2 12631 zaddcl 12657 qre 12995 qaddcl 13007 qnegcl 13008 qmulcl 13009 qreccl 13011 elpqb 13018 hash2prd 14514 elss2prb 14527 fundmge2nop0 14541 wrdl3s3 15001 replim 15155 prodmo 15972 odd2np1 16378 opoe 16400 omoe 16401 opeo 16402 omeo 16403 qredeu 16695 pythagtriplem1 16854 pcz 16919 4sqlem1 16986 4sqlem2 16987 4sqlem4 16990 mul4sq 16992 pmtr3ncom 19493 efgmnvl 19732 efgrelexlema 19767 ring1ne0 20296 pzriprnglem8 21499 txuni2 23573 tx2ndc 23659 blssioo 24816 tgioo 24817 ioorf 25608 ioorinv 25611 ioorcl 25612 dyaddisj 25631 mbfid 25670 elply 26234 vmacl 27161 efvmacl 27163 vmalelog 27249 2sqlem2 27462 mul2sq 27463 2sqlem7 27468 2sqnn0 27482 2sqreultblem 27492 pntibnd 27637 ostth 27683 scutf 27857 zaddscl 28380 zmulscld 28383 elzn0s 28384 eln0zs 28386 zseo 28406 elzs12 28421 zs12bday 28424 remulscllem1 28432 legval 28592 upgredgpr 29159 nbgr2vtx1edg 29367 cusgredg 29441 usgredgsscusgredg 29477 wwlksnwwlksnon 29935 n4cyclfrgr 30310 vdgn1frgrv2 30315 friendshipgt3 30417 lpni 30499 nsnlplig 30500 nsnlpligALT 30501 n0lpligALT 30503 ipasslem5 30854 ipasslem11 30859 hhssnv 31283 shscli 31336 shsleji 31389 shsidmi 31403 spansncvi 31671 superpos 32373 chirredi 32413 mdsymlem6 32427 rnmposs 32684 1fldgenq 33324 ccfldextdgrr 33722 cnre2csqima 33910 dya2icobrsiga 34278 dya2iocnrect 34283 dya2iocucvr 34286 sxbrsigalem2 34288 afsval 34686 satfv0 35363 satfrnmapom 35375 satfv0fun 35376 satf00 35379 sat1el2xp 35384 fmla0xp 35388 fmla1 35392 msubco 35536 elaltxp 35976 altxpsspw 35978 funtransport 36032 funray 36141 funline 36143 ellines 36153 linethru 36154 icoreresf 37353 icoreclin 37358 relowlssretop 37364 relowlpssretop 37365 itg2addnc 37681 isline 39741 sn-it0e0 42445 sn-mullid 42465 sn-0tie0 42469 sn-mul02 42470 mzpcompact2lem 42762 sprvalpw 47467 sprvalpwn0 47470 prsprel 47474 prpair 47488 prprvalpw 47502 reuopreuprim 47513 nnsum3primesgbe 47779 nnsum4primesodd 47783 nnsum4primesoddALTV 47784 tgblthelfgott 47802 grtrif1o 47909 grtrissvtx 47911 gpgvtxel2 48006 nnpw2pb 48508 2arymaptf1 48574 |
| Copyright terms: Public domain | W3C validator |