Theorem eu2ndop1stv

Description: If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017)

	Ref	Expression
Assertion	eu2ndop1stv	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		euex	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 )
2		nfeu1	⊢ Ⅎ 𝑦 ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉
3		nfcv	⊢ Ⅎ 𝑦 𝐴
4	3	nfel1	⊢ Ⅎ 𝑦 𝐴 ∈ V
5	2 4	nfim	⊢ Ⅎ 𝑦 ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → 𝐴 ∈ V )
6		opprc1	⊢ ( ¬ 𝐴 ∈ V → ⟨ 𝐴 , 𝑦 ⟩ = ∅ )
7	6	eleq1d	⊢ ( ¬ 𝐴 ∈ V → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ↔ ∅ ∈ 𝑉 ) )
8		ax-5	⊢ ( ∅ ∈ 𝑉 → ∀ 𝑦 ∅ ∈ 𝑉 )
9		alneu	⊢ ( ∀ 𝑦 ∅ ∈ 𝑉 → ¬ ∃! 𝑦 ∅ ∈ 𝑉 )
10	8 9	syl	⊢ ( ∅ ∈ 𝑉 → ¬ ∃! 𝑦 ∅ ∈ 𝑉 )
11	7 10	syl6bi	⊢ ( ¬ 𝐴 ∈ V → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → ¬ ∃! 𝑦 ∅ ∈ 𝑉 ) )
12	11	impcom	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ∧ ¬ 𝐴 ∈ V ) → ¬ ∃! 𝑦 ∅ ∈ 𝑉 )
13	7	eubidv	⊢ ( ¬ 𝐴 ∈ V → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ↔ ∃! 𝑦 ∅ ∈ 𝑉 ) )
14	13	notbid	⊢ ( ¬ 𝐴 ∈ V → ( ¬ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ↔ ¬ ∃! 𝑦 ∅ ∈ 𝑉 ) )
15	14	adantl	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ∧ ¬ 𝐴 ∈ V ) → ( ¬ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ↔ ¬ ∃! 𝑦 ∅ ∈ 𝑉 ) )
16	12 15	mpbird	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ∧ ¬ 𝐴 ∈ V ) → ¬ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 )
17	16	ex	⊢ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → ( ¬ 𝐴 ∈ V → ¬ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 ) )
18	17	con4d	⊢ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → 𝐴 ∈ V ) )
19	5 18	exlimi	⊢ ( ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → 𝐴 ∈ V ) )
20	1 19	mpcom	⊢ ( ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝑉 → 𝐴 ∈ V )