Theorem 2rexbidv 3209

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	rexbidv 3171	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3171	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-rex 3071

This theorem is referenced by:  f1oiso  7272  elrnmpog  7463  elrnmpo  7464  ralrnmpo  7466  ovelrn  7502  opiota  7959  omeu  8479  oeeui  8496  eroveu  8664  erov  8666  elfiun  9279  dffi3  9280  xpwdomg  9434  brdom7disj  10380  brdom6disj  10381  genpv  10848  genpelv  10849  axcnre  11013  supadd  12036  supmullem1  12038  supmullem2  12039  supmul  12040  sqrlem6  15050  ello1  15315  ello1mpt  15321  elo1  15326  lo1o1  15332  o1lo1  15337  bezoutlem1  16338  bezoutlem3  16340  bezoutlem4  16341  bezout  16342  pythagtriplem2  16607  pythagtriplem19  16623  pythagtrip  16624  pcval  16634  pceu  16636  pczpre  16637  pcdiv  16642  4sqlem2  16739  4sqlem3  16740  4sqlem4  16742  4sq  16754  vdwlem1  16771  vdwlem12  16782  vdwlem13  16783  vdwnnlem1  16785  vdwnnlem2  16786  vdwnnlem3  16787  vdwnn  16788  ramub2  16804  rami  16805  cat1lem  17900  cat1  17901  pgpfac1lem3  19767  lspprel  20454  znunit  20869  cayleyhamiltonALT  22138  hausnei  22577  isreg2  22626  txuni2  22814  txbas  22816  xkoopn  22838  txcls  22853  txcnpi  22857  txdis1cn  22884  txtube  22889  txcmplem1  22890  hausdiag  22894  tx1stc  22899  regr1lem2  22989  qustgplem  23370  met2ndci  23776  dyadmax  24860  i1fadd  24957  i1fmul  24958  elply  25454  2sqlem2  26664  2sqlem8  26672  2sqlem9  26673  2sqlem11  26675  istrkgld  27050  istrkg3ld  27052  axtgupdim2  27062  axtgeucl  27063  legov  27176  iscgra  27400  dfcgra2  27421  axsegconlem1  27515  axpasch  27539  axlowdim  27559  axeuclidlem  27560  nb3grpr  27979  upgr4cycl4dv4e  28778  vdgn1frgrv2  28889  fusgr2wsp2nb  28927  l2p  29070  br8d  31178  pstmval  32084  eulerpartlemgh  32586  eulerpartlemgs2  32588  cvmliftlem15  33500  cvmlift2lem10  33514  satf  33555  satfv0  33560  satfrnmapom  33572  satfv0fun  33573  satf0op  33579  sat1el2xp  33581  fmlafvel  33587  fmla1  33589  fmlaomn0  33592  gonan0  33594  goaln0  33595  gonar  33597  goalr  33599  fmlasucdisj  33601  satffunlem2lem1  33606  dmopab3rexdif  33607  satfv0fvfmla0  33615  sategoelfvb  33621  satfv1fvfmla1  33625  2goelgoanfmla1  33626  br8  33956  br6  33957  br4  33958  elmade  34142  elaltxp  34368  brsegle  34501  ellines  34545  nn0prpwlem  34602  nn0prpw  34603  ptrest  35874  ismblfin  35916  itg2addnclem3  35928  itg2addnc  35929  releldmqscoss  36920  isline  38000  psubspi  38008  paddfval  38058  elpadd  38060  paddvaln0N  38062  3rspcedvd  40432  flt4lem7  40746  nna4b4nsq  40747  mzpcompact2lem  40823  mzpcompact2  40824  sbc4rexgOLD  40862  pell1qrval  40918  elpell1qr  40919  pell14qrval  40920  elpell14qr  40921  pell1234qrval  40922  elpell1234qr  40923  jm2.27  41081  expdiophlem1  41094  clsk1independent  41966  limclner  43517  fourierdlem42  44015  fourierdlem48  44020  sprel  45276  prelspr  45278  prprelb  45308  prprelprb  45309  reuprpr  45315  isgbe  45543  isgbow  45544  isgbo  45545  sbgoldbalt  45573  sgoldbeven3prm  45575  mogoldbb  45577  sbgoldbo  45579  nnsum3primesle9  45586  bigoval  46235  elbigo  46237  iscnrm3r  46582  iscnrm3l  46585