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  5962  elrnmpog  6129  elrnmpo  6130  ralrnmpo  6131  rexrnmpo  6132  ovelrn  6166  eroveu  6790  genipv  7719  genpelxp  7721  genpelvl  7722  genpelvu  7723  axcnre  8091  apreap  8757  apreim  8773  aprcl  8816  aptap  8820  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  pythagtriplem19  12845  pceu  12858  pcval  12859  pczpre  12860  pcdiv  12865  4sqlem2  12952  4sqlem3  12953  4sqlem4  12955  4sqexercise2  12962  4sqlemsdc  12963  4sq  12973  znunit  14663  txuni2  14970  txbas  14972  txdis1cn  14992  elply  15448  2sqlem2  15834  2sqlem8  15842  2sqlem9  15843  upgredg  15983  3dom  16523