Theorem 2rexbidv 2519

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2478

This theorem is referenced by:  f1oiso  5869  elrnmpog  6031  elrnmpo  6032  ralrnmpo  6033  rexrnmpo  6034  ovelrn  6067  eroveu  6680  genipv  7569  genpelxp  7571  genpelvl  7572  genpelvu  7573  axcnre  7941  apreap  8606  apreim  8622  aprcl  8665  aptap  8669  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  pythagtriplem19  12420  pceu  12433  pcval  12434  pczpre  12435  pcdiv  12440  4sqlem2  12527  4sqlem3  12528  4sqlem4  12530  4sqexercise2  12537  4sqlemsdc  12538  4sq  12548  znunit  14147  txuni2  14424  txbas  14426  txdis1cn  14446  elply  14880  2sqlem2  15202  2sqlem8  15210  2sqlem9  15211