| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspc2ev | Structured version Visualization version GIF version | ||
| Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.) |
| Ref | Expression |
|---|---|
| rspc2v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
| rspc2v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rspc2ev | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspc2v.2 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
| 2 | 1 | rspcev 3622 | . . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒) |
| 3 | 2 | anim2i 617 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒)) |
| 4 | 3 | 3impb 1115 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒)) |
| 5 | rspc2v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 6 | 5 | rexbidv 3179 | . . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒)) |
| 7 | 6 | rspcev 3622 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
| 8 | 4, 7 | syl 17 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ 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 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: 2rspcedvdw 3636 rspc3ev 3639 opelxp 5721 fprb 7214 f1prex 7304 nf1const 7324 rspceov 7480 erov 8854 ralxpmap 8936 2dom 9070 elfiun 9470 dffi3 9471 ixpiunwdom 9630 1re 11261 hashdmpropge2 14522 wrdl2exs2 14985 ello12r 15553 ello1d 15559 elo12r 15564 o1lo1 15573 addcn2 15630 mulcn2 15632 bezoutlem3 16578 bezout 16580 pythagtriplem18 16870 pczpre 16885 pcdiv 16890 4sqlem3 16988 4sqlem4 16990 4sqlem12 16994 vdwlem1 17019 vdwlem6 17024 vdwlem8 17026 vdwlem12 17030 vdwlem13 17031 0ram 17058 ramz2 17062 cat1lem 18141 sgrp2rid2ex 18940 pmtr3ncom 19493 psgnunilem1 19511 irredn0 20423 isnzr2 20518 hausnei2 23361 cnhaus 23362 dishaus 23390 ordthauslem 23391 txuni2 23573 xkoopn 23597 txopn 23610 txdis 23640 txdis1cn 23643 pthaus 23646 txhaus 23655 tx1stc 23658 xkohaus 23661 regr1lem 23747 qustgplem 24129 methaus 24533 met2ndci 24535 metnrmlem3 24883 elplyr 26240 aaliou2b 26383 aaliou3lem9 26392 2irrexpq 26773 2irrexpqALT 26843 2sqlem2 27462 2sqlem8 27470 2sqlem11 27473 2sqb 27476 2sqnn0 27482 2sqnn 27483 pntibnd 27637 madecut 27921 mulsproplem12 28153 precsexlem11 28241 zzs12 28423 remulscllem1 28432 legov 28593 iscgrad 28819 f1otrge 28880 axsegconlem1 28932 axsegcon 28942 axpaschlem 28955 axlowdimlem6 28962 axlowdim1 28974 axlowdim2 28975 axeuclidlem 28977 umgrvad2edg 29230 wwlksnwwlksnon 29935 upgr4cycl4dv4e 30204 3cyclfrgrrn1 30304 4cycl2vnunb 30309 br8d 32622 lt2addrd 32755 xlt2addrd 32762 xrnarchi 33191 txomap 33833 tpr2rico 33911 qqhval2 33983 elsx 34195 br2base 34271 dya2iocnrect 34283 connpconn 35240 satfv1fvfmla1 35428 br8 35756 br4 35758 brsegle 36109 hilbert1.1 36155 nn0prpwlem 36323 knoppndvlem21 36533 poimirlem1 37628 itg2addnclem3 37680 cntotbnd 37803 smprngopr 38059 3dim2 39470 llni2 39514 lvoli3 39579 lvoli2 39583 islinei 39742 psubspi2N 39750 elpaddri 39804 eldioph2lem1 42771 diophin 42783 fphpdo 42828 irrapxlem3 42835 irrapxlem4 42836 pellexlem6 42845 pell1234qrreccl 42865 pell1234qrmulcl 42866 pell1234qrdich 42872 pell1qr1 42882 pellqrexplicit 42888 rmxycomplete 42929 dgraalem 43157 tfsconcatrev 43361 clsk3nimkb 44053 fourierdlem64 46185 rspceaov 47209 ichnreuop 47459 prelspr 47473 reuopreuprim 47513 6gbe 47758 7gbow 47759 8gbe 47760 9gbo 47761 11gbo 47762 modn0mul 48441 elbigo2r 48474 rrx2xpref1o 48639 inlinecirc02plem 48707 sepfsepc 48825 iscnrm3lem7 48836 |
| Copyright terms: Public domain | W3C validator |