Theorem eldm3

Description: Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017)

	Ref	Expression
Assertion	eldm3	⊢ ( 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ dom 𝐵 → 𝐴 ∈ V )
2		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
3		reseq2	⊢ ( { 𝐴 } = ∅ → ( 𝐵 ↾ { 𝐴 } ) = ( 𝐵 ↾ ∅ ) )
4		res0	⊢ ( 𝐵 ↾ ∅ ) = ∅
5	3 4	eqtrdi	⊢ ( { 𝐴 } = ∅ → ( 𝐵 ↾ { 𝐴 } ) = ∅ )
6	2 5	sylbi	⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ↾ { 𝐴 } ) = ∅ )
7	6	necon1ai	⊢ ( ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ → 𝐴 ∈ V )
8		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ dom 𝐵 ↔ 𝐴 ∈ dom 𝐵 ) )
9		sneq	⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
10	9	reseq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ↾ { 𝑥 } ) = ( 𝐵 ↾ { 𝐴 } ) )
11	10	neeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ ) )
12		dfclel	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
13	12	exbii	⊢ ( ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ↔ ∃ 𝑦 ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
14		vex	⊢ 𝑥 ∈ V
15	14	eldm2	⊢ ( 𝑥 ∈ dom 𝐵 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
16		n0	⊢ ( ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) )
17		elres	⊢ ( 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) ↔ ∃ 𝑧 ∈ { 𝑥 } ∃ 𝑦 ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) )
18		eleq1	⊢ ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ → ( 𝑝 ∈ 𝐵 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) )
19	18	pm5.32i	⊢ ( ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ↔ ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) )
20		opeq1	⊢ ( 𝑧 = 𝑥 → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
21	20	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ↔ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) )
22	21	anbi1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ) )
23	19 22	bitr3id	⊢ ( 𝑧 = 𝑥 → ( ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ) )
24	23	exbidv	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ) )
25	14 24	rexsn	⊢ ( ∃ 𝑧 ∈ { 𝑥 } ∃ 𝑦 ( 𝑝 = ⟨ 𝑧 , 𝑦 ⟩ ∧ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
26	17 25	bitri	⊢ ( 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) ↔ ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
27	26	exbii	⊢ ( ∃ 𝑝 𝑝 ∈ ( 𝐵 ↾ { 𝑥 } ) ↔ ∃ 𝑝 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
28		excom	⊢ ( ∃ 𝑝 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
29	16 27 28	3bitri	⊢ ( ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑝 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑝 ∈ 𝐵 ) )
30	13 15 29	3bitr4i	⊢ ( 𝑥 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝑥 } ) ≠ ∅ )
31	8 11 30	vtoclbg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ ) )
32	1 7 31	pm5.21nii	⊢ ( 𝐴 ∈ dom 𝐵 ↔ ( 𝐵 ↾ { 𝐴 } ) ≠ ∅ )