Theorem 2rexbidv 3227

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 3186	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3186	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  f1oiso  7335  elrnmpog  7531  elrnmpo  7532  ralrnmpo  7535  ovelrn  7572  opiota  8040  omeu  8554  oeeui  8572  eroveu  8794  erov  8796  elfiun  9376  dffi3  9377  xpwdomg  9533  brdom7disj  10488  brdom6disj  10489  genpv  10957  genpelv  10958  axcnre  11122  supadd  12160  supmullem1  12162  supmullem2  12163  supmul  12164  01sqrexlem6  15274  ello1  15542  ello1mpt  15548  elo1  15553  lo1o1  15559  o1lo1  15564  bezoutlem1  16573  bezoutlem3  16575  bezoutlem4  16576  bezout  16577  pythagtriplem2  16853  pythagtriplem19  16869  pythagtrip  16870  pcval  16880  pceu  16882  pczpre  16883  pcdiv  16888  4sqlem2  16985  4sqlem3  16986  4sqlem4  16988  4sq  17000  vdwlem1  17017  vdwlem12  17028  vdwlem13  17029  vdwnnlem1  17031  vdwnnlem2  17032  vdwnnlem3  17033  vdwnn  17034  ramub2  17050  rami  17051  cat1lem  18129  cat1  18130  pgpfac1lem3  20119  lspprel  21158  znunit  21612  cayleyhamiltonALT  22948  hausnei  23385  isreg2  23434  txuni2  23622  txbas  23624  xkoopn  23646  txcls  23661  txcnpi  23665  txdis1cn  23692  txtube  23697  txcmplem1  23698  hausdiag  23702  tx1stc  23707  regr1lem2  23797  qustgplem  24178  met2ndci  24579  dyadmax  25657  i1fadd  25754  i1fmul  25755  elply  26252  2sqlem2  27479  2sqlem8  27487  2sqlem9  27488  2sqlem11  27490  elmade  27947  mulsval  28199  mulsval2lem  28200  mulsproplem9  28214  mulsproplem12  28217  sltmuls1  28237  sltmuls2  28238  mulsuniflem  28239  addsdilem2  28242  mulsasslem1  28253  mulsasslem2  28254  mulsunif2  28260  precsexlemcbv  28296  precsexlem9  28305  precsexlem11  28307  eucliddivs  28466  bdayfinbndcbv  28556  bdayfinbndlem1  28557  bdayfinbndlem2  28558  bdayfinbnd  28559  elz12s  28562  z12zsodd  28572  z12sge0  28573  remulscllem1  28590  istrkgld  28625  istrkg3ld  28627  axtgupdim2  28637  axtgeucl  28638  legov  28751  iscgra  29000  dfcgra2  29021  axsegconlem1  29115  axpasch  29139  axlowdim  29159  axeuclidlem  29160  nb3grpr  29580  upgr4cycl4dv4e  30384  vdgn1frgrv2  30495  fusgr2wsp2nb  30533  l2p  30679  br8d  32807  gsumwun  33253  constrsuc  34032  constrsslem  34035  constrconj  34039  constrllcllem  34046  constrlccllem  34047  constrcccllem  34048  constrcbvlem  34049  pstmval  34189  eulerpartlemgh  34672  eulerpartlemgs2  34674  cvmliftlem15  35645  cvmlift2lem10  35659  satf  35700  satfv0  35705  satfrnmapom  35717  satfv0fun  35718  satf0op  35724  sat1el2xp  35726  fmlafvel  35732  fmla1  35734  fmlaomn0  35737  gonan0  35739  goaln0  35740  gonar  35742  goalr  35744  fmlasucdisj  35746  satffunlem2lem1  35751  dmopab3rexdif  35752  satfv0fvfmla0  35760  sategoelfvb  35766  satfv1fvfmla1  35770  2goelgoanfmla1  35771  br8  36103  br6  36104  br4  36105  elaltxp  36322  brsegle  36455  ellines  36499  nn0prpwlem  36679  nn0prpw  36680  ptrest  38115  ismblfin  38157  itg2addnclem3  38169  itg2addnc  38170  releldmqscoss  39241  isline  40360  psubspi  40368  paddfval  40418  elpadd  40420  paddvaln0N  40422  3rspcedvd  42832  flt4lem7  43238  nna4b4nsq  43239  mzpcompact2lem  43329  mzpcompact2  43330  pell1qrval  43420  elpell1qr  43421  pell14qrval  43422  elpell14qr  43423  pell1234qrval  43424  elpell1234qr  43425  jm2.27  43582  expdiophlem1  43595  oenord1  43890  oaun3lem1  43948  clsk1independent  44619  limclner  46222  fourierdlem42  46720  fourierdlem48  46725  sprel  48087  prelspr  48089  prprelb  48119  prprelprb  48120  reuprpr  48126  isgbe  48370  isgbow  48371  isgbo  48372  sbgoldbalt  48400  sgoldbeven3prm  48402  mogoldbb  48404  sbgoldbo  48406  nnsum3primesle9  48413  usgrgrtrirex  48569  grlimgrtri  48622  grlimedgnedg  48750  bigoval  49168  elbigo  49170  iscnrm3r  49566  iscnrm3l  49569