Theorem rspc2ev 3648

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2ev	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2ev

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
2	1	rspcev 3635	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 616	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1115	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3185	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3635	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077

This theorem is referenced by:  2rspcedvdw  3649  rspc3ev  3652  opelxp  5736  fprb  7231  f1prex  7320  nf1const  7340  rspceov  7497  erov  8872  ralxpmap  8954  2dom  9095  elfiun  9499  dffi3  9500  ixpiunwdom  9659  1re  11290  hashdmpropge2  14532  wrdl2exs2  14995  ello12r  15563  ello1d  15569  elo12r  15574  o1lo1  15583  addcn2  15640  mulcn2  15642  bezoutlem3  16588  bezout  16590  pythagtriplem18  16879  pczpre  16894  pcdiv  16899  4sqlem3  16997  4sqlem4  16999  4sqlem12  17003  vdwlem1  17028  vdwlem6  17033  vdwlem8  17035  vdwlem12  17039  vdwlem13  17040  0ram  17067  ramz2  17071  cat1lem  18163  sgrp2rid2ex  18962  pmtr3ncom  19517  psgnunilem1  19535  irredn0  20449  isnzr2  20544  hausnei2  23382  cnhaus  23383  dishaus  23411  ordthauslem  23412  txuni2  23594  xkoopn  23618  txopn  23631  txdis  23661  txdis1cn  23664  pthaus  23667  txhaus  23676  tx1stc  23679  xkohaus  23682  regr1lem  23768  qustgplem  24150  methaus  24554  met2ndci  24556  metnrmlem3  24902  elplyr  26260  aaliou2b  26401  aaliou3lem9  26410  2irrexpq  26791  2irrexpqALT  26861  2sqlem2  27480  2sqlem8  27488  2sqlem11  27491  2sqb  27494  2sqnn0  27500  2sqnn  27501  pntibnd  27655  madecut  27939  mulsproplem12  28171  precsexlem11  28259  zzs12  28441  remulscllem1  28450  legov  28611  iscgrad  28837  f1otrge  28898  axsegconlem1  28950  axsegcon  28960  axpaschlem  28973  axlowdimlem6  28980  axlowdim1  28992  axlowdim2  28993  axeuclidlem  28995  umgrvad2edg  29248  wwlksnwwlksnon  29948  upgr4cycl4dv4e  30217  3cyclfrgrrn1  30317  4cycl2vnunb  30322  br8d  32632  lt2addrd  32758  xlt2addrd  32765  xrnarchi  33164  txomap  33780  tpr2rico  33858  qqhval2  33928  elsx  34158  br2base  34234  dya2iocnrect  34246  connpconn  35203  satfv1fvfmla1  35391  br8  35718  br4  35720  brsegle  36072  hilbert1.1  36118  nn0prpwlem  36288  knoppndvlem21  36498  poimirlem1  37581  itg2addnclem3  37633  cntotbnd  37756  smprngopr  38012  3dim2  39425  llni2  39469  lvoli3  39534  lvoli2  39538  islinei  39697  psubspi2N  39705  elpaddri  39759  eldioph2lem1  42716  diophin  42728  fphpdo  42773  irrapxlem3  42780  irrapxlem4  42781  pellexlem6  42790  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell1234qrdich  42817  pell1qr1  42827  pellqrexplicit  42833  rmxycomplete  42874  dgraalem  43102  tfsconcatrev  43310  clsk3nimkb  44002  fourierdlem64  46091  rspceaov  47112  ichnreuop  47346  prelspr  47360  reuopreuprim  47400  6gbe  47645  7gbow  47646  8gbe  47647  9gbo  47648  11gbo  47649  modn0mul  48254  elbigo2r  48287  rrx2xpref1o  48452  inlinecirc02plem  48520  sepfsepc  48607  iscnrm3lem7  48619