Theorem rexbidv2 3224

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 1924	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3070	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3070	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3070

This theorem is referenced by:  rexbidva  3225  rexeqbidv  3337  rexss  3992  exopxfr2  5753  isoini  7209  rexsupp  7998  omabs  8481  elfi2  9173  wemapsolem  9309  ltexpi  10658  rexuz  12638  ncoprmgcdne1b  16355  lpigen  20527  llyi  22625  nllyi  22626  elpi1  24208  ressupprn  31024  xrecex  31194  bnj18eq1  32907  ldual1dim  37180  pmapjat1  37867  mrefg2  40529  islssfg2  40896  fourierdlem71  43718  hoiqssbl  44163  lubeldm2d  46252  glbeldm2d  46253