Theorem rexab 3716

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.) Reduce axiom usage. (Revised by GG, 2-Nov-2024.)

Hypothesis

Ref	Expression
ralab.1	⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rexab	⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒))

Distinct variable groups:   𝑥,𝑦   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑥,𝑦)

Proof of Theorem rexab

Step	Hyp	Ref	Expression
1		dfrex2 3079	. . . 4 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒)
2		ralab.1	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
3	2	ralab 3713	. . . 4 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒))
4	1, 3	xchbinx 334	. . 3 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒))
5		imnang 1840	. . 3 ⊢ (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓 ∧ 𝜒))
6	4, 5	xchbinx 334	. 2 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒))
7		df-ex 1778	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒))
8	6, 7	bitr4i 278	1 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535  ∃wex 1777  {cab 2717  ∀wral 3067  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-ral 3068  df-rex 3077

This theorem is referenced by:  4sqlem12  17003  noinfno  27781  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  renegscl  28448  readdscl  28449  remulscl  28452  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnc  37634  diophrex  42731