Theorem releldm2

Description: Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013)

	Ref	Expression
Assertion	releldm2	⊢ ( Rel 𝐴 → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐵 ∈ dom 𝐴 → 𝐵 ∈ V )
2	1	anim2i	⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ dom 𝐴 ) → ( Rel 𝐴 ∧ 𝐵 ∈ V ) )
3		id	⊢ ( ( 1st ‘ 𝑥 ) = 𝐵 → ( 1st ‘ 𝑥 ) = 𝐵 )
4		fvex	⊢ ( 1st ‘ 𝑥 ) ∈ V
5	3 4	eqeltrrdi	⊢ ( ( 1st ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
6	5	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
7	6	anim2i	⊢ ( ( Rel 𝐴 ∧ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) → ( Rel 𝐴 ∧ 𝐵 ∈ V ) )
8		eldm2g	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ) )
9	8	adantl	⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ) )
10		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
11		ssel	⊢ ( 𝐴 ⊆ ( V × V ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( V × V ) ) )
12	10 11	sylbi	⊢ ( Rel 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( V × V ) ) )
13	12	imp	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( V × V ) )
14		op1steq	⊢ ( 𝑥 ∈ ( V × V ) → ( ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
15	13 14	syl	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
16	15	rexbidva	⊢ ( Rel 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
17	16	adantr	⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ) )
18		rexcom4	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ )
19		risset	⊢ ( ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ )
20	19	exbii	⊢ ( ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ )
21	18 20	bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 = ⟨ 𝐵 , 𝑦 ⟩ ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 )
22	17 21	bitrdi	⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑦 ⟨ 𝐵 , 𝑦 ⟩ ∈ 𝐴 ) )
23	9 22	bitr4d	⊢ ( ( Rel 𝐴 ∧ 𝐵 ∈ V ) → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) )
24	2 7 23	pm5.21nd	⊢ ( Rel 𝐴 → ( 𝐵 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1st ‘ 𝑥 ) = 𝐵 ) )