Theorem 2rexbidv 2567

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2526

This theorem is referenced by:  f1oiso  5999  elrnmpog  6166  elrnmpo  6167  ralrnmpo  6168  rexrnmpo  6169  ovelrn  6203  eroveu  6860  genipv  7824  genpelxp  7826  genpelvl  7827  genpelvu  7828  axcnre  8196  apreap  8861  apreim  8877  aprcl  8920  aptap  8924  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  pythagtriplem19  12980  pceu  12993  pcval  12994  pczpre  12995  pcdiv  13000  4sqlem2  13087  4sqlem3  13088  4sqlem4  13090  4sqexercise2  13097  4sqlemsdc  13098  4sq  13108  znunit  14807  txuni2  15121  txbas  15123  txdis1cn  15143  elply  15599  2sqlem2  15988  2sqlem8  15996  2sqlem9  15997  upgredg  16139  3dom  16762