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  5894  elrnmpog  6057  elrnmpo  6058  ralrnmpo  6059  rexrnmpo  6060  ovelrn  6094  eroveu  6712  genipv  7621  genpelxp  7623  genpelvl  7624  genpelvu  7625  axcnre  7993  apreap  8659  apreim  8675  aprcl  8718  aptap  8722  bezoutlemnewy  12288  bezoutlema  12291  bezoutlemb  12292  pythagtriplem19  12576  pceu  12589  pcval  12590  pczpre  12591  pcdiv  12596  4sqlem2  12683  4sqlem3  12684  4sqlem4  12686  4sqexercise2  12693  4sqlemsdc  12694  4sq  12704  znunit  14392  txuni2  14699  txbas  14701  txdis1cn  14721  elply  15177  2sqlem2  15563  2sqlem8  15571  2sqlem9  15572