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  12259  bezoutlema  12262  bezoutlemb  12263  pythagtriplem19  12547  pceu  12560  pcval  12561  pczpre  12562  pcdiv  12567  4sqlem2  12654  4sqlem3  12655  4sqlem4  12657  4sqexercise2  12664  4sqlemsdc  12665  4sq  12675  znunit  14363  txuni2  14670  txbas  14672  txdis1cn  14692  elply  15148  2sqlem2  15534  2sqlem8  15542  2sqlem9  15543