Theorem rspc2ev 3592

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.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2	1	rexbidv 3190	. 2 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
3		simp1 1154	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4		rspc2v.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcev 3580	. . 3 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
6	5	3adant1 1148	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
7	2, 3, 6	rspcedvdw 3583	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091

This theorem is used by:  2rspcedvdw  3593  opelxp  5691  fprb  7222  f1prex  7315  nf1const  7335  rspceov  7492  erov  8863  ralxpmap  8952  2dom  9086  elfiun  9449  dffi3  9450  ixpiunwdom  9611  1re  11335  hashdmpropge2  14655  wrdl2exs2  15126  ello12r  15713  ello1d  15719  elo12r  15724  o1lo1  15733  addcn2  15790  mulcn2  15792  bezoutlem3  16743  bezout  16745  pythagtriplem18  17039  pczpre  17054  pcdiv  17059  4sqlem3  17157  4sqlem4  17159  4sqlem12  17163  vdwlem1  17188  vdwlem6  17193  vdwlem8  17195  vdwlem12  17199  vdwlem13  17200  0ram  17227  ramz2  17231  cat1lem  18300  sgrp2rid2ex  19155  pmtr3ncom  19719  psgnunilem1  19737  irredn0  20683  isnzr2  20798  hausnei2  23701  cnhaus  23702  dishaus  23730  ordthauslem  23731  txuni2  23914  xkoopn  23938  txopn  23951  txdis  23981  txdis1cn  23984  pthaus  23987  txhaus  23996  tx1stc  23999  xkohaus  24002  regr1lem  24088  qustgplem  24470  methaus  24869  met2ndci  24871  metnrmlem3  25211  elplyr  26549  aaliou2b  26698  aaliou3lem9  26707  2irrexpq  27089  2irrexpqALT  27158  2sqlem2  27775  2sqlem8  27783  2sqlem11  27786  2sqb  27789  2sqnn  27796  pntibnd  27950  madecut  28299  mulsproplem12  28543  precsexlem11  28633  eucliddivs  28792  elz12si  28889  zz12s  28891  remulscllem1  28916  legov  29078  iscgrad  29348  f1otrge  29479  axsegconlem1  29525  axsegcon  29535  axpaschlem  29548  axlowdimlem6  29555  axlowdim1  29567  axlowdim2  29568  axeuclidlem  29570  umgrvad2edg  29824  wwlksnwwlksnon  30534  upgr4cycl4dv4e  30816  3cyclfrgrrn1  30916  4cycl2vnunb  30921  br8d  33274  lt2addrd  33412  xlt2addrd  33421  xrnarchi  33815  txomap  34536  tpr2rico  34614  qqhval2  34684  elsx  34897  br2base  34971  dya2iocnrect  34983  connpconn  36167  satfv1fvfmla1  36355  br8  36699  br4  36701  brsegle  37051  hilbert1.1  37097  nn0prpwlem  37288  knoppndvlem21  37576  poimirlem1  38731  itg2addnclem3  38783  cntotbnd  38922  smprngopr  39178  3dim2  40717  llni2  40761  lvoli3  40826  lvoli2  40830  islinei  40989  psubspi2N  40997  elpaddri  41051  eldioph2lem1  43964  diophin  43976  fphpdo  44017  irrapxlem3  44024  irrapxlem4  44025  pellexlem6  44034  pell1234qrreccl  44054  pell1234qrmulcl  44055  pell1234qrdich  44061  pell1qr1  44071  pellqrexplicit  44077  rmxycomplete  44117  dgraalem  44339  tfsconcatrev  44542  clsk3nimkb  45232  fourierdlem64  47385  rspceaov  48472  modn0mul  48638  ichnreuop  48759  prelspr  48773  reuopreuprim  48813  6gbe  49074  7gbow  49075  8gbe  49076  9gbo  49077  11gbo  49078  smprngprmrng  49641  elbigo2r  49870  inlinecirc02plem  50103  sepfsepc  50247  iscnrm3lem7  50258