Theorem hashrabsn1

Description: If the size of a restricted class abstraction restricted to a singleton is 1, the condition of the class abstraction must hold for the singleton. (Contributed by Alexander van der Vekens, 3-Sep-2018)

	Ref	Expression
Assertion	hashrabsn1	⊢ ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 }
2		rabrsn	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) )
3		fveqeq2	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 ↔ ( ♯ ‘ ∅ ) = 1 ) )
4		hash0	⊢ ( ♯ ‘ ∅ ) = 0
5	4	eqeq1i	⊢ ( ( ♯ ‘ ∅ ) = 1 ↔ 0 = 1 )
6		0ne1	⊢ 0 ≠ 1
7		eqneqall	⊢ ( 0 = 1 → ( 0 ≠ 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
8	6 7	mpi	⊢ ( 0 = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
9	5 8	sylbi	⊢ ( ( ♯ ‘ ∅ ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
10	3 9	biimtrdi	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
11		snidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝐴 } )
12	11	adantr	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → 𝐴 ∈ { 𝐴 } )
13		eleq2	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ 𝐴 ∈ { 𝐴 } ) )
14	13	adantl	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ 𝐴 ∈ { 𝐴 } ) )
15	12 14	mpbird	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } )
16		nfcv	⊢ Ⅎ 𝑥 { 𝐴 }
17	16	elrabsf	⊢ ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ ( 𝐴 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
18	17	simprbi	⊢ ( 𝐴 ∈ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → [ 𝐴 / 𝑥 ] 𝜑 )
19	15 18	syl	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → [ 𝐴 / 𝑥 ] 𝜑 )
20	19	a1d	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
21	20	ex	⊢ ( 𝐴 ∈ V → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
22		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
23		eqeq2	⊢ ( { 𝐴 } = ∅ → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ↔ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ) )
24		ax-1ne0	⊢ 1 ≠ 0
25		eqneqall	⊢ ( 1 = 0 → ( 1 ≠ 0 → [ 𝐴 / 𝑥 ] 𝜑 ) )
26	24 25	mpi	⊢ ( 1 = 0 → [ 𝐴 / 𝑥 ] 𝜑 )
27	26	eqcoms	⊢ ( 0 = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
28	5 27	sylbi	⊢ ( ( ♯ ‘ ∅ ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )
29	3 28	biimtrdi	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
30	23 29	biimtrdi	⊢ ( { 𝐴 } = ∅ → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
31	22 30	sylbi	⊢ ( ¬ 𝐴 ∈ V → ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
32	21 31	pm2.61i	⊢ ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
33	10 32	jaoi	⊢ ( ( { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = ∅ ∨ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝐴 } ) → ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 ) )
34	1 2 33	mp2b	⊢ ( ( ♯ ‘ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ) = 1 → [ 𝐴 / 𝑥 ] 𝜑 )