Theorem 2rexbidv 2530

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

Syntax hints:   → wi 4   ↔ wb 105  ∃wrex 2484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-rex 2489

This theorem is referenced by:  f1oiso  5885  elrnmpog  6048  elrnmpo  6049  ralrnmpo  6050  rexrnmpo  6051  ovelrn  6085  eroveu  6703  genipv  7604  genpelxp  7606  genpelvl  7607  genpelvu  7608  axcnre  7976  apreap  8642  apreim  8658  aprcl  8701  aptap  8705  bezoutlemnewy  12236  bezoutlema  12239  bezoutlemb  12240  pythagtriplem19  12524  pceu  12537  pcval  12538  pczpre  12539  pcdiv  12544  4sqlem2  12631  4sqlem3  12632  4sqlem4  12634  4sqexercise2  12641  4sqlemsdc  12642  4sq  12652  znunit  14339  txuni2  14646  txbas  14648  txdis1cn  14668  elply  15124  2sqlem2  15510  2sqlem8  15518  2sqlem9  15519