Theorem acexmidlema 5423

Description: Lemma for acexmid 5431. (Contributed by Jim Kingdon, 6-Aug-2019.)

Hypotheses

Ref	Expression
acexmidlem.a	⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
acexmidlem.b	⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨ φ)}
acexmidlem.c	⊢ 𝐶 = {A, B}

Assertion

Ref	Expression
acexmidlema	⊢ ({∅} ∈ A → φ)

Distinct variable groups:   x,A   x,B   x,𝐶   φ,x

Proof of Theorem acexmidlema

Step	Hyp	Ref	Expression
1		acexmidlem.a	. . . 4 ⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)}
2	1	eleq2i 2082	. . 3 ⊢ ({∅} ∈ A ↔ {∅} ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)})
3		p0ex 3909	. . . . 5 ⊢ {∅} ∈ V
4	3	prid2 3447	. . . 4 ⊢ {∅} ∈ {∅, {∅}}
5		eqeq1 2024	. . . . . 6 ⊢ (x = {∅} → (x = ∅ ↔ {∅} = ∅))
6	5	orbi1d 692	. . . . 5 ⊢ (x = {∅} → ((x = ∅ ∨ φ) ↔ ({∅} = ∅ ∨ φ)))
7	6	elrab3 2672	. . . 4 ⊢ ({∅} ∈ {∅, {∅}} → ({∅} ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} ↔ ({∅} = ∅ ∨ φ)))
8	4, 7	ax-mp 7	. . 3 ⊢ ({∅} ∈ {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} ↔ ({∅} = ∅ ∨ φ))
9	2, 8	bitri 173	. 2 ⊢ ({∅} ∈ A ↔ ({∅} = ∅ ∨ φ))
10		noel 3201	. . . 4 ⊢ ¬ ∅ ∈ ∅
11		0ex 3854	. . . . . 6 ⊢ ∅ ∈ V
12	11	snid 3373	. . . . 5 ⊢ ∅ ∈ {∅}
13		eleq2 2079	. . . . 5 ⊢ ({∅} = ∅ → (∅ ∈ {∅} ↔ ∅ ∈ ∅))
14	12, 13	mpbii 136	. . . 4 ⊢ ({∅} = ∅ → ∅ ∈ ∅)
15	10, 14	mto 575	. . 3 ⊢ ¬ {∅} = ∅
16		orel1 631	. . 3 ⊢ (¬ {∅} = ∅ → (({∅} = ∅ ∨ φ) → φ))
17	15, 16	ax-mp 7	. 2 ⊢ (({∅} = ∅ ∨ φ) → φ)
18	9, 17	sylbi 114	1 ⊢ ({∅} ∈ A → φ)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 98   ∨ wo 616   = wceq 1226   ∈ wcel 1370  {crab 2284  ∅c0 3197  {csn 3346  {cpr 3347

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-nul 3853  ax-pow 3897

This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-rab 2289  df-v 2533  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-sn 3352  df-pr 3353

This theorem is referenced by:  acexmidlem1  5428