Theorem 2rexbidv 2575

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used by:  f1oiso  6032  elrnmpog  6201  elrnmpo  6202  ralrnmpo  6203  rexrnmpo  6204  ovelrn  6238  eroveu  6900  genipv  7877  genpelxp  7879  genpelvl  7880  genpelvu  7881  axcnre  8249  apreap  8918  apreim  8934  aprcl  8977  aptap  8981  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  pythagtriplem19  13084  pceu  13097  pcval  13098  pczpre  13099  pcdiv  13104  4sqlem2  13191  4sqlem3  13192  4sqlem4  13194  4sqexercise2  13201  4sqlemsdc  13202  4sq  13212  znunit  15085  txuni2  15456  txbas  15458  txdis1cn  15478  elply  15934  2sqlem2  16413  2sqlem8  16421  2sqlem9  16422  upgredg  16564  3dom  17197