Theorem rexbidv2 3187

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3092

This theorem is used by:  rexbidva  3189  rexeqbidv  3341  rexssOLD  4014  iuneq12d  4988  exopxfr2  5832  isoini  7342  rexsupp  8180  omabs  8639  elfi2  9377  wemapsolem  9515  ltexpi  10898  rexuz  12934  ncoprmgcdne1b  16726  lpigen  21533  llyi  23662  nllyi  23663  elpi1  25235  ressupprn  33082  xrecex  33285  constrcbvlem  34185  bnj18eq1  35356  ldual1dim  39973  pmapjat1  40660  mrefg2  43471  islssfg2  43831  fourierdlem71  46924  hoiqssbl  47372  reuxfr1dd  49618  lubeldm2d  49769  glbeldm2d  49770