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 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

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

This theorem is referenced by:  f1oiso  6022  elrnmpog  6191  elrnmpo  6192  ralrnmpo  6193  rexrnmpo  6194  ovelrn  6228  eroveu  6890  genipv  7866  genpelxp  7868  genpelvl  7869  genpelvu  7870  axcnre  8238  apreap  8905  apreim  8921  aprcl  8964  aptap  8968  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  pythagtriplem19  13039  pceu  13052  pcval  13053  pczpre  13054  pcdiv  13059  4sqlem2  13146  4sqlem3  13147  4sqlem4  13149  4sqexercise2  13156  4sqlemsdc  13157  4sq  13167  znunit  14966  txuni2  15280  txbas  15282  txdis1cn  15302  elply  15758  2sqlem2  16148  2sqlem8  16156  2sqlem9  16157  upgredg  16299  3dom  16932