Theorem rexbidv2 3162

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1778   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-rex 3060

This theorem is referenced by:  rexbidva  3164  rexeqbidv  3330  rexssOLD  4041  iuneq12d  5001  exopxfr2  5835  isoini  7340  rexsupp  8189  omabs  8671  elfi2  9436  wemapsolem  9572  ltexpi  10924  rexuz  12922  ncoprmgcdne1b  16669  lpigen  21307  llyi  23428  nllyi  23429  elpi1  25014  ressupprn  32634  xrecex  32842  constrcbvlem  33735  bnj18eq1  34900  ldual1dim  39126  pmapjat1  39814  mrefg2  42681  islssfg2  43046  fourierdlem71  46149  hoiqssbl  46597  reuxfr1dd  48684  lubeldm2d  48815  glbeldm2d  48816