Theorem elold

Description: Membership in an old set. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	elold	Could not format assertion : No typesetting found for |- ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oldval	Could not format ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) : No typesetting found for |- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) with typecode |-
2	1	eleq2d	Could not format ( A e. On -> ( X e. ( _Old ` A ) <-> X e. U. ( _Made " A ) ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _Old ` A ) <-> X e. U. ( _Made " A ) ) ) with typecode |-
3		eluni	Could not format ( X e. U. ( _Made " A ) <-> E. y ( X e. y /\ y e. ( _Made " A ) ) ) : No typesetting found for |- ( X e. U. ( _Made " A ) <-> E. y ( X e. y /\ y e. ( _Made " A ) ) ) with typecode |-
4		madef	Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
5		ffn	Could not format ( _Made : On --> ~P No -> _Made Fn On ) : No typesetting found for |- ( _Made : On --> ~P No -> _Made Fn On ) with typecode |-
6	4 5	ax-mp	Could not format _Made Fn On : No typesetting found for |- _Made Fn On with typecode |-
7		onss	$$⊢A\in \mathrm{On}\to A\subseteq \mathrm{On}$$
8		fvelimab	Could not format ( ( _Made Fn On /\ A C_ On ) -> ( y e. ( _Made " A ) <-> E. b e. A ( _Made ` b ) = y ) ) : No typesetting found for |- ( ( _Made Fn On /\ A C_ On ) -> ( y e. ( _Made " A ) <-> E. b e. A ( _Made ` b ) = y ) ) with typecode |-
9	6 7 8	sylancr	Could not format ( A e. On -> ( y e. ( _Made " A ) <-> E. b e. A ( _Made ` b ) = y ) ) : No typesetting found for |- ( A e. On -> ( y e. ( _Made " A ) <-> E. b e. A ( _Made ` b ) = y ) ) with typecode |-
10	9	anbi2d	Could not format ( A e. On -> ( ( X e. y /\ y e. ( _Made " A ) ) <-> ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) ) : No typesetting found for |- ( A e. On -> ( ( X e. y /\ y e. ( _Made " A ) ) <-> ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) ) with typecode |-
11	10	exbidv	Could not format ( A e. On -> ( E. y ( X e. y /\ y e. ( _Made " A ) ) <-> E. y ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) ) : No typesetting found for |- ( A e. On -> ( E. y ( X e. y /\ y e. ( _Made " A ) ) <-> E. y ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) ) with typecode |-
12		fvex	Could not format ( _Made ` b ) e. _V : No typesetting found for |- ( _Made ` b ) e. _V with typecode |-
13	12	clel3	Could not format ( X e. ( _Made ` b ) <-> E. y ( y = ( _Made ` b ) /\ X e. y ) ) : No typesetting found for |- ( X e. ( _Made ` b ) <-> E. y ( y = ( _Made ` b ) /\ X e. y ) ) with typecode |-
14	13	rexbii	Could not format ( E. b e. A X e. ( _Made ` b ) <-> E. b e. A E. y ( y = ( _Made ` b ) /\ X e. y ) ) : No typesetting found for |- ( E. b e. A X e. ( _Made ` b ) <-> E. b e. A E. y ( y = ( _Made ` b ) /\ X e. y ) ) with typecode |-
15		rexcom4	Could not format ( E. b e. A E. y ( y = ( _Made ` b ) /\ X e. y ) <-> E. y E. b e. A ( y = ( _Made ` b ) /\ X e. y ) ) : No typesetting found for |- ( E. b e. A E. y ( y = ( _Made ` b ) /\ X e. y ) <-> E. y E. b e. A ( y = ( _Made ` b ) /\ X e. y ) ) with typecode |-
16		eqcom	Could not format ( y = ( _Made ` b ) <-> ( _Made ` b ) = y ) : No typesetting found for |- ( y = ( _Made ` b ) <-> ( _Made ` b ) = y ) with typecode |-
17	16	anbi2ci	Could not format ( ( y = ( _Made ` b ) /\ X e. y ) <-> ( X e. y /\ ( _Made ` b ) = y ) ) : No typesetting found for |- ( ( y = ( _Made ` b ) /\ X e. y ) <-> ( X e. y /\ ( _Made ` b ) = y ) ) with typecode |-
18	17	rexbii	Could not format ( E. b e. A ( y = ( _Made ` b ) /\ X e. y ) <-> E. b e. A ( X e. y /\ ( _Made ` b ) = y ) ) : No typesetting found for |- ( E. b e. A ( y = ( _Made ` b ) /\ X e. y ) <-> E. b e. A ( X e. y /\ ( _Made ` b ) = y ) ) with typecode |-
19		r19.42v	Could not format ( E. b e. A ( X e. y /\ ( _Made ` b ) = y ) <-> ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) : No typesetting found for |- ( E. b e. A ( X e. y /\ ( _Made ` b ) = y ) <-> ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) with typecode |-
20	18 19	bitri	Could not format ( E. b e. A ( y = ( _Made ` b ) /\ X e. y ) <-> ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) : No typesetting found for |- ( E. b e. A ( y = ( _Made ` b ) /\ X e. y ) <-> ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) with typecode |-
21	20	exbii	Could not format ( E. y E. b e. A ( y = ( _Made ` b ) /\ X e. y ) <-> E. y ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) : No typesetting found for |- ( E. y E. b e. A ( y = ( _Made ` b ) /\ X e. y ) <-> E. y ( X e. y /\ E. b e. A ( _Made ` b ) = y ) ) with typecode |-
22	14 15 21	3bitrri	Could not format ( E. y ( X e. y /\ E. b e. A ( _Made ` b ) = y ) <-> E. b e. A X e. ( _Made ` b ) ) : No typesetting found for |- ( E. y ( X e. y /\ E. b e. A ( _Made ` b ) = y ) <-> E. b e. A X e. ( _Made ` b ) ) with typecode |-
23	11 22	bitrdi	Could not format ( A e. On -> ( E. y ( X e. y /\ y e. ( _Made " A ) ) <-> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( A e. On -> ( E. y ( X e. y /\ y e. ( _Made " A ) ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
24	3 23	bitrid	Could not format ( A e. On -> ( X e. U. ( _Made " A ) <-> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( A e. On -> ( X e. U. ( _Made " A ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
25	2 24	bitrd	Could not format ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-