Theorem 2rexbidv 2522

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  f1oiso  5876  elrnmpog  6039  elrnmpo  6040  ralrnmpo  6041  rexrnmpo  6042  ovelrn  6076  eroveu  6694  genipv  7595  genpelxp  7597  genpelvl  7598  genpelvu  7599  axcnre  7967  apreap  8633  apreim  8649  aprcl  8692  aptap  8696  bezoutlemnewy  12190  bezoutlema  12193  bezoutlemb  12194  pythagtriplem19  12478  pceu  12491  pcval  12492  pczpre  12493  pcdiv  12498  4sqlem2  12585  4sqlem3  12586  4sqlem4  12588  4sqexercise2  12595  4sqlemsdc  12596  4sq  12606  znunit  14293  txuni2  14600  txbas  14602  txdis1cn  14622  elply  15078  2sqlem2  15464  2sqlem8  15472  2sqlem9  15473