Theorem 2rexbidv 3242

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

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem 2rexbidv

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

Syntax hints:   → wi 4   ↔ wb 198  ∃wrex 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-rex 3096

This theorem is referenced by:  f1oiso  6875  elrnmpt2g  7051  elrnmpt2  7052  ralrnmpt2  7054  ovelrn  7089  opiota  7510  omeu  7951  oeeui  7968  eroveu  8128  erov  8130  elfiun  8626  dffi3  8627  xpwdomg  8781  brdom7disj  9690  brdom6disj  9691  genpv  10158  genpelv  10159  axcnre  10323  supadd  11349  supmullem1  11351  supmullem2  11352  supmul  11353  sqrlem6  14399  ello1  14658  ello1mpt  14664  elo1  14669  lo1o1  14675  o1lo1  14680  bezoutlem1  15666  bezoutlem3  15668  bezoutlem4  15669  bezout  15670  pythagtriplem2  15930  pythagtriplem19  15946  pythagtrip  15947  pcval  15957  pceu  15959  pczpre  15960  pcdiv  15965  4sqlem2  16061  4sqlem3  16062  4sqlem4  16064  4sq  16076  vdwlem1  16093  vdwlem12  16104  vdwlem13  16105  vdwnnlem1  16107  vdwnnlem2  16108  vdwnnlem3  16109  vdwnn  16110  ramub2  16126  rami  16127  pgpfac1lem3  18867  lspprel  19493  znunit  20311  cayleyhamiltonALT  21107  hausnei  21544  isreg2  21593  txuni2  21781  txbas  21783  xkoopn  21805  txcls  21820  txcnpi  21824  txdis1cn  21851  txtube  21856  txcmplem1  21857  hausdiag  21861  tx1stc  21866  regr1lem2  21956  qustgplem  22336  met2ndci  22739  dyadmax  23806  i1fadd  23903  i1fmul  23904  elply  24392  2sqlem2  25599  2sqlem8  25607  2sqlem9  25608  2sqlem11  25610  istrkgld  25814  axtgeucl  25827  legov  25940  iscgra  26161  dfcgra2  26182  axsegconlem1  26270  axpasch  26294  axlowdim  26314  axeuclidlem  26315  nb3grpr  26734  upgr4cycl4dv4e  27592  vdgn1frgrv2  27708  fusgr2wsp2nb  27746  l2p  27910  br8d  29989  pstmval  30540  eulerpartlemgh  31042  eulerpartlemgs2  31044  cvmliftlem15  31883  cvmlift2lem10  31897  br8  32244  br6  32245  br4  32246  elaltxp  32675  brsegle  32808  ellines  32852  nn0prpwlem  32909  nn0prpw  32910  ptrest  34039  ismblfin  34081  itg2addnclem3  34093  itg2addnc  34094  isline  35898  psubspi  35906  paddfval  35956  elpadd  35958  paddvaln0N  35960  3rspcedvd  38125  mzpcompact2lem  38284  mzpcompact2  38285  sbc4rexgOLD  38324  pell1qrval  38380  elpell1qr  38381  pell14qrval  38382  elpell14qr  38383  pell1234qrval  38384  elpell1234qr  38385  jm2.27  38544  expdiophlem1  38557  clsk1independent  39310  limclner  40801  fourierdlem42  41303  fourierdlem48  41308  sprel  42433  prelspr  42435  prprelb  42465  prprelprb  42466  isgbe  42674  isgbow  42675  isgbo  42676  sbgoldbalt  42704  sgoldbeven3prm  42706  mogoldbb  42708  sbgoldbo  42710  nnsum3primesle9  42717  bigoval  43368  elbigo  43370