Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) Add disjoint variable condition to avoid ax-13 . See bnj1441g for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bnj1441.1 | |- ( x e. A -> A. y x e. A ) |
|
bnj1441.2 | |- ( ph -> A. y ph ) |
||
Assertion | bnj1441 | |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bnj1441.1 | |- ( x e. A -> A. y x e. A ) |
|
2 | bnj1441.2 | |- ( ph -> A. y ph ) |
|
3 | df-rab | |- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
|
4 | 1 2 | hban | |- ( ( x e. A /\ ph ) -> A. y ( x e. A /\ ph ) ) |
5 | 4 | hbab | |- ( z e. { x | ( x e. A /\ ph ) } -> A. y z e. { x | ( x e. A /\ ph ) } ) |
6 | 3 5 | hbxfreq | |- ( z e. { x e. A | ph } -> A. y z e. { x e. A | ph } ) |