Theorem elnoOLD

Description: Obsolete version of elno as of 5-Jun-2025. (Contributed by Scott Fenton, 11-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elnoOLD	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ No → 𝐴 ∈ V )
2		fex	⊢ ( ( 𝐴 : 𝑥 ⟶ { 1o , 2o } ∧ 𝑥 ∈ On ) → 𝐴 ∈ V )
3	2	ancoms	⊢ ( ( 𝑥 ∈ On ∧ 𝐴 : 𝑥 ⟶ { 1o , 2o } ) → 𝐴 ∈ V )
4	3	rexlimiva	⊢ ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } → 𝐴 ∈ V )
5		feq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ 𝐴 : 𝑥 ⟶ { 1o , 2o } ) )
6	5	rexbidv	⊢ ( 𝑓 = 𝐴 → ( ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } ) )
7		df-no	⊢ No = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } }
8	6 7	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } ) )
9	1 4 8	pm5.21nii	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )