Theorem 2rexbidv 2555

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-rex 2514

This theorem is referenced by:  f1oiso  5956  elrnmpog  6123  elrnmpo  6124  ralrnmpo  6125  rexrnmpo  6126  ovelrn  6160  eroveu  6781  genipv  7707  genpelxp  7709  genpelvl  7710  genpelvu  7711  axcnre  8079  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  bezoutlemnewy  12532  bezoutlema  12535  bezoutlemb  12536  pythagtriplem19  12820  pceu  12833  pcval  12834  pczpre  12835  pcdiv  12840  4sqlem2  12927  4sqlem3  12928  4sqlem4  12930  4sqexercise2  12937  4sqlemsdc  12938  4sq  12948  znunit  14638  txuni2  14945  txbas  14947  txdis1cn  14967  elply  15423  2sqlem2  15809  2sqlem8  15817  2sqlem9  15818  upgredg  15957  3dom  16411