Theorem 2rexbidv 2557

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  f1oiso  5967  elrnmpog  6134  elrnmpo  6135  ralrnmpo  6136  rexrnmpo  6137  ovelrn  6171  eroveu  6795  genipv  7729  genpelxp  7731  genpelvl  7732  genpelvu  7733  axcnre  8101  apreap  8767  apreim  8783  aprcl  8826  aptap  8830  bezoutlemnewy  12572  bezoutlema  12575  bezoutlemb  12576  pythagtriplem19  12860  pceu  12873  pcval  12874  pczpre  12875  pcdiv  12880  4sqlem2  12967  4sqlem3  12968  4sqlem4  12970  4sqexercise2  12977  4sqlemsdc  12978  4sq  12988  znunit  14679  txuni2  14986  txbas  14988  txdis1cn  15008  elply  15464  2sqlem2  15850  2sqlem8  15858  2sqlem9  15859  upgredg  16001  3dom  16613