Theorem 2rexbidv 2558

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2517

This theorem is referenced by:  f1oiso  5977  elrnmpog  6144  elrnmpo  6145  ralrnmpo  6146  rexrnmpo  6147  ovelrn  6181  eroveu  6838  genipv  7772  genpelxp  7774  genpelvl  7775  genpelvu  7776  axcnre  8144  apreap  8809  apreim  8825  aprcl  8868  aptap  8872  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  pythagtriplem19  12918  pceu  12931  pcval  12932  pczpre  12933  pcdiv  12938  4sqlem2  13025  4sqlem3  13026  4sqlem4  13028  4sqexercise2  13035  4sqlemsdc  13036  4sq  13046  znunit  14738  txuni2  15050  txbas  15052  txdis1cn  15072  elply  15528  2sqlem2  15917  2sqlem8  15925  2sqlem9  15926  upgredg  16068  3dom  16691