Theorem rr-grothshort

Description: A shorter equivalent of ax-groth than rr-groth using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024)

	Ref	Expression
Assertion	rr-grothshort	|- E. y ( x e. y /\ A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )

Proof

Step	Hyp	Ref	Expression
1		gruex	|- E. y e. Univ x e. y
2	1	ax-gen	|- A. x E. y e. Univ x e. y
3		rr-grothshortbi	|- ( A. x E. y e. Univ x e. y <-> A. x E. y ( x e. y /\ A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) ) )
4	2 3	mpbi	|- A. x E. y ( x e. y /\ A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
5	4	spi	|- E. y ( x e. y /\ A. z e. y A. f e. ~P y E. w e. y ( ~P z C_ ( y i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )