![]() |
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 3582 | . . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒) |
3 | 2 | anim2i 618 | . . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒)) |
4 | 3 | 3impb 1116 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒)) |
5 | rspc2v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
6 | 5 | rexbidv 3176 | . . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒)) |
7 | 6 | rspcev 3582 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
8 | 4, 7 | syl 17 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ 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 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-3an 1090 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 |
This theorem is referenced by: rspc3ev 3595 opelxp 5670 fprb 7144 f1prex 7231 nf1const 7251 rspceov 7405 erov 8754 ralxpmap 8835 2dom 8975 elfiun 9367 dffi3 9368 ixpiunwdom 9527 1re 11156 hashdmpropge2 14383 wrdl2exs2 14836 ello12r 15400 ello1d 15406 elo12r 15411 o1lo1 15420 addcn2 15477 mulcn2 15479 bezoutlem3 16423 bezout 16425 pythagtriplem18 16705 pczpre 16720 pcdiv 16725 4sqlem3 16823 4sqlem4 16825 4sqlem12 16829 vdwlem1 16854 vdwlem6 16859 vdwlem8 16861 vdwlem12 16865 vdwlem13 16866 0ram 16893 ramz2 16897 cat1lem 17983 sgrp2rid2ex 18738 pmtr3ncom 19258 psgnunilem1 19276 irredn0 20133 isnzr2 20736 hausnei2 22707 cnhaus 22708 dishaus 22736 ordthauslem 22737 txuni2 22919 xkoopn 22943 txopn 22956 txdis 22986 txdis1cn 22989 pthaus 22992 txhaus 23001 tx1stc 23004 xkohaus 23007 regr1lem 23093 qustgplem 23475 methaus 23879 met2ndci 23881 metnrmlem3 24227 elplyr 25565 aaliou2b 25704 aaliou3lem9 25713 2irrexpq 26088 2irrexpqALT 26153 2sqlem2 26769 2sqlem8 26777 2sqlem11 26780 2sqb 26783 2sqnn0 26789 2sqnn 26790 pntibnd 26944 madecut 27215 legov 27530 iscgrad 27756 f1otrge 27817 axsegconlem1 27869 axsegcon 27879 axpaschlem 27892 axlowdimlem6 27899 axlowdim1 27911 axlowdim2 27912 axeuclidlem 27914 umgrvad2edg 28164 wwlksnwwlksnon 28863 upgr4cycl4dv4e 29132 3cyclfrgrrn1 29232 4cycl2vnunb 29237 br8d 31532 lt2addrd 31659 xlt2addrd 31666 xrnarchi 32023 txomap 32418 tpr2rico 32496 qqhval2 32566 elsx 32796 br2base 32872 dya2iocnrect 32884 connpconn 33832 satfv1fvfmla1 34020 br8 34332 br4 34334 brsegle 34696 hilbert1.1 34742 nn0prpwlem 34797 knoppndvlem21 34998 poimirlem1 36082 itg2addnclem3 36134 cntotbnd 36258 smprngopr 36514 3dim2 37934 llni2 37978 lvoli3 38043 lvoli2 38047 islinei 38206 psubspi2N 38214 elpaddri 38268 2rspcedvdw 40635 eldioph2lem1 41086 diophin 41098 fphpdo 41143 irrapxlem3 41150 irrapxlem4 41151 pellexlem6 41160 pell1234qrreccl 41180 pell1234qrmulcl 41181 pell1234qrdich 41187 pell1qr1 41197 pellqrexplicit 41203 rmxycomplete 41244 dgraalem 41475 clsk3nimkb 42319 fourierdlem64 44418 rspceaov 45436 ichnreuop 45671 prelspr 45685 reuopreuprim 45725 6gbe 45970 7gbow 45971 8gbe 45972 9gbo 45973 11gbo 45974 modn0mul 46613 elbigo2r 46646 rrx2xpref1o 46811 inlinecirc02plem 46879 sepfsepc 46967 iscnrm3lem7 46979 |
Copyright terms: Public domain | W3C validator |