Theorem 2rexbidv 2557

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  f1oiso  5966  elrnmpog  6133  elrnmpo  6134  ralrnmpo  6135  rexrnmpo  6136  ovelrn  6170  eroveu  6794  genipv  7728  genpelxp  7730  genpelvl  7731  genpelvu  7732  axcnre  8100  apreap  8766  apreim  8782  aprcl  8825  aptap  8829  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  pythagtriplem19  12854  pceu  12867  pcval  12868  pczpre  12869  pcdiv  12874  4sqlem2  12961  4sqlem3  12962  4sqlem4  12964  4sqexercise2  12971  4sqlemsdc  12972  4sq  12982  znunit  14672  txuni2  14979  txbas  14981  txdis1cn  15001  elply  15457  2sqlem2  15843  2sqlem8  15851  2sqlem9  15852  upgredg  15994  3dom  16587