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  7593  genpelxp  7595  genpelvl  7596  genpelvu  7597  axcnre  7965  apreap  8631  apreim  8647  aprcl  8690  aptap  8694  bezoutlemnewy  12188  bezoutlema  12191  bezoutlemb  12192  pythagtriplem19  12476  pceu  12489  pcval  12490  pczpre  12491  pcdiv  12496  4sqlem2  12583  4sqlem3  12584  4sqlem4  12586  4sqexercise2  12593  4sqlemsdc  12594  4sq  12604  znunit  14291  txuni2  14576  txbas  14578  txdis1cn  14598  elply  15054  2sqlem2  15440  2sqlem8  15448  2sqlem9  15449