Theorem 2rexbidv 2532

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-rex 2491

This theorem is referenced by:  f1oiso  5908  elrnmpog  6071  elrnmpo  6072  ralrnmpo  6073  rexrnmpo  6074  ovelrn  6108  eroveu  6726  genipv  7642  genpelxp  7644  genpelvl  7645  genpelvu  7646  axcnre  8014  apreap  8680  apreim  8696  aprcl  8739  aptap  8743  bezoutlemnewy  12392  bezoutlema  12395  bezoutlemb  12396  pythagtriplem19  12680  pceu  12693  pcval  12694  pczpre  12695  pcdiv  12700  4sqlem2  12787  4sqlem3  12788  4sqlem4  12790  4sqexercise2  12797  4sqlemsdc  12798  4sq  12808  znunit  14496  txuni2  14803  txbas  14805  txdis1cn  14825  elply  15281  2sqlem2  15667  2sqlem8  15675  2sqlem9  15676