Theorem qliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016) (Revised by AV, 3-Aug-2024)

	Ref	Expression
Hypotheses	qlift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
	qlift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
	qlift.3	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
	qlift.4	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	qliftel	⊢ ( 𝜑 → ( [ 𝐶 ] 𝑅 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qlift.1	⊢ 𝐹 = ran ( 𝑥 ∈ 𝑋 ↦ ⟨ [ 𝑥 ] 𝑅 , 𝐴 ⟩ )
2		qlift.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑌 )
3		qlift.3	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
4		qlift.4	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5	1 2 3 4	qliftlem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] 𝑅 ∈ ( 𝑋 / 𝑅 ) )
6	1 5 2	fliftel	⊢ ( 𝜑 → ( [ 𝐶 ] 𝑅 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ∧ 𝐷 = 𝐴 ) ) )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑅 Er 𝑋 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
9	7 8	erth2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐶 𝑅 𝑥 ↔ [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ) )
10	9	anbi1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ↔ ( [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ∧ 𝐷 = 𝐴 ) ) )
11	10	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝑋 ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑋 ( [ 𝐶 ] 𝑅 = [ 𝑥 ] 𝑅 ∧ 𝐷 = 𝐴 ) ) )
12	6 11	bitr4d	⊢ ( 𝜑 → ( [ 𝐶 ] 𝑅 𝐹 𝐷 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝐶 𝑅 𝑥 ∧ 𝐷 = 𝐴 ) ) )