Theorem rexab 3650

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 3060	. . . 4 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒)
2		ralab.1	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
3	2	ralab 3648	. . . 4 ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜑} ¬ 𝜒 ↔ ∀𝑥(𝜓 → ¬ 𝜒))
4	1, 3	xchbinx 334	. . 3 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥(𝜓 → ¬ 𝜒))
5		imnang 1843	. . 3 ⊢ (∀𝑥(𝜓 → ¬ 𝜒) ↔ ∀𝑥 ¬ (𝜓 ∧ 𝜒))
6	4, 5	xchbinx 334	. 2 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒))
7		df-ex 1781	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜒) ↔ ¬ ∀𝑥 ¬ (𝜓 ∧ 𝜒))
8	6, 7	bitr4i 278	1 ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜑}𝜒 ↔ ∃𝑥(𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780  {cab 2711  ∀wral 3048  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-ral 3049  df-rex 3058

This theorem is referenced by:  4sqlem12  16870  noinfno  27658  sleadd1  27933  addsuniflem  27945  addsasslem1  27947  addsasslem2  27948  mulsuniflem  28089  addsdilem1  28091  addsdilem2  28092  mulsasslem1  28103  mulsasslem2  28104  renegscl  28401  readdscl  28402  remulscl  28405  mblfinlem3  37719  mblfinlem4  37720  ismblfin  37721  itg2addnclem  37731  itg2addnc  37734  diophrex  42892