Theorem bj-elgab

Description: Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-elgab.nf	$$⊢\phi \to \forall x\phi$$
	bj-elgab.nfa	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	bj-elgab.ex	$$⊢\phi \to A\in V$$
	bj-elgab.is	$$⊢\phi \to \left(\exists x\left(A=B\wedge \psi \right)\leftrightarrow \chi \right)$$
Assertion	bj-elgab	Could not format assertion : No typesetting found for |- ( ph -> ( A e. {{ B | x | ps }} <-> ch ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bj-elgab.nf	$$⊢\phi \to \forall x\phi$$
2		bj-elgab.nfa	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
3		bj-elgab.ex	$$⊢\phi \to A\in V$$
4		bj-elgab.is	$$⊢\phi \to \left(\exists x\left(A=B\wedge \psi \right)\leftrightarrow \chi \right)$$
5		df-bj-gab	Could not format {{ B | x | ps }} = { y | E. x ( B = y /\ ps ) } : No typesetting found for |- {{ B | x | ps }} = { y | E. x ( B = y /\ ps ) } with typecode |-
6	5	eleq2i	Could not format ( A e. {{ B | x | ps }} <-> A e. { y | E. x ( B = y /\ ps ) } ) : No typesetting found for |- ( A e. {{ B | x | ps }} <-> A e. { y | E. x ( B = y /\ ps ) } ) with typecode |-
7	1	adantr	$$⊢\left(\phi \wedge y=A\right)\to \forall x\phi$$
8		nfcvd	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xy$$
9		id	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xA$$
10	8 9	nfeqd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy=A$$
11	10	nf5rd	$$⊢\underset{\_}{Ⅎ}xA\to \left(y=A\to \forall xy=A\right)$$
12	2 11	syl	$$⊢\phi \to \left(y=A\to \forall xy=A\right)$$
13	12	imp	$$⊢\left(\phi \wedge y=A\right)\to \forall xy=A$$
14		19.26	$$⊢\forall x\left(\phi \wedge y=A\right)\leftrightarrow \left(\forall x\phi \wedge \forall xy=A\right)$$
15	7 13 14	sylanbrc	$$⊢\left(\phi \wedge y=A\right)\to \forall x\left(\phi \wedge y=A\right)$$
16		eqeq2	$$⊢y=A\to \left(B=y\leftrightarrow B=A\right)$$
17		eqcom	$$⊢B=A\leftrightarrow A=B$$
18	16 17	bitrdi	$$⊢y=A\to \left(B=y\leftrightarrow A=B\right)$$
19	18	anbi1d	$$⊢y=A\to \left(\left(B=y\wedge \psi \right)\leftrightarrow \left(A=B\wedge \psi \right)\right)$$
20	19	adantl	$$⊢\left(\phi \wedge y=A\right)\to \left(\left(B=y\wedge \psi \right)\leftrightarrow \left(A=B\wedge \psi \right)\right)$$
21	15 20	exbidh	$$⊢\left(\phi \wedge y=A\right)\to \left(\exists x\left(B=y\wedge \psi \right)\leftrightarrow \exists x\left(A=B\wedge \psi \right)\right)$$
22	21	ex	$$⊢\phi \to \left(y=A\to \left(\exists x\left(B=y\wedge \psi \right)\leftrightarrow \exists x\left(A=B\wedge \psi \right)\right)\right)$$
23	22	alrimiv	$$⊢\phi \to \forall y\left(y=A\to \left(\exists x\left(B=y\wedge \psi \right)\leftrightarrow \exists x\left(A=B\wedge \psi \right)\right)\right)$$
24		elabgt	$$⊢\left(A\in V\wedge \forall y\left(y=A\to \left(\exists x\left(B=y\wedge \psi \right)\leftrightarrow \exists x\left(A=B\wedge \psi \right)\right)\right)\right)\to \left(A\in \left\{y|\exists x\left(B=y\wedge \psi \right)\right\}\leftrightarrow \exists x\left(A=B\wedge \psi \right)\right)$$
25	3 23 24	syl2anc	$$⊢\phi \to \left(A\in \left\{y|\exists x\left(B=y\wedge \psi \right)\right\}\leftrightarrow \exists x\left(A=B\wedge \psi \right)\right)$$
26	25 4	bitrd	$$⊢\phi \to \left(A\in \left\{y|\exists x\left(B=y\wedge \psi \right)\right\}\leftrightarrow \chi \right)$$
27	6 26	bitrid	Could not format ( ph -> ( A e. {{ B | x | ps }} <-> ch ) ) : No typesetting found for |- ( ph -> ( A e. {{ B | x | ps }} <-> ch ) ) with typecode |-