Metamath Proof Explorer


Theorem unissbOLD

Description: Obsolete version of unissb as of 28-Dec-2024. (Contributed by NM, 20-Sep-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion unissbOLD
|- ( U. A C_ B <-> A. x e. A x C_ B )

Proof

Step Hyp Ref Expression
1 eluni
 |-  ( y e. U. A <-> E. x ( y e. x /\ x e. A ) )
2 1 imbi1i
 |-  ( ( y e. U. A -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
3 19.23v
 |-  ( A. x ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( E. x ( y e. x /\ x e. A ) -> y e. B ) )
4 2 3 bitr4i
 |-  ( ( y e. U. A -> y e. B ) <-> A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
5 4 albii
 |-  ( A. y ( y e. U. A -> y e. B ) <-> A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) )
6 alcom
 |-  ( A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. x A. y ( ( y e. x /\ x e. A ) -> y e. B ) )
7 19.21v
 |-  ( A. y ( x e. A -> ( y e. x -> y e. B ) ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
8 impexp
 |-  ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( y e. x -> ( x e. A -> y e. B ) ) )
9 bi2.04
 |-  ( ( y e. x -> ( x e. A -> y e. B ) ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
10 8 9 bitri
 |-  ( ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> ( y e. x -> y e. B ) ) )
11 10 albii
 |-  ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. y ( x e. A -> ( y e. x -> y e. B ) ) )
12 dfss2
 |-  ( x C_ B <-> A. y ( y e. x -> y e. B ) )
13 12 imbi2i
 |-  ( ( x e. A -> x C_ B ) <-> ( x e. A -> A. y ( y e. x -> y e. B ) ) )
14 7 11 13 3bitr4i
 |-  ( A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> ( x e. A -> x C_ B ) )
15 14 albii
 |-  ( A. x A. y ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
16 6 15 bitri
 |-  ( A. y A. x ( ( y e. x /\ x e. A ) -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
17 5 16 bitri
 |-  ( A. y ( y e. U. A -> y e. B ) <-> A. x ( x e. A -> x C_ B ) )
18 dfss2
 |-  ( U. A C_ B <-> A. y ( y e. U. A -> y e. B ) )
19 df-ral
 |-  ( A. x e. A x C_ B <-> A. x ( x e. A -> x C_ B ) )
20 17 18 19 3bitr4i
 |-  ( U. A C_ B <-> A. x e. A x C_ B )