Theorem rexbidv2 3223

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
rexbidv2.1	⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))

Assertion

Ref	Expression
rexbidv2	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem rexbidv2

Step	Hyp	Ref	Expression
1		rexbidv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
2	1	exbidv 1925	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3bitr4g 313	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-rex 3069

This theorem is referenced by:  rexbidva  3224  rexeqbidv  3328  rexss  3988  exopxfr2  5742  isoini  7189  rexsupp  7969  omabs  8441  elfi2  9103  wemapsolem  9239  ltexpi  10589  rexuz  12567  ncoprmgcdne1b  16283  lpigen  20440  llyi  22533  nllyi  22534  elpi1  24114  ressupprn  30926  xrecex  31096  bnj18eq1  32807  ldual1dim  37107  pmapjat1  37794  mrefg2  40445  islssfg2  40812  fourierdlem71  43608  hoiqssbl  44053  lubeldm2d  46140  glbeldm2d  46141