Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Rohan Ridenour
Shorter primitive equivalent of ax-groth
Grothendieck universes are closed under collection
elscottab
Metamath Proof Explorer
Description: An element of the output of the Scott operation applied to a class
abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour , 14-Aug-2023)
Ref
Expression
Hypothesis
elscottab.1
⊢ x = y → φ ↔ ψ
Assertion
elscottab
⊢ y ∈ Scott x | φ → ψ
Proof
Step
Hyp
Ref
Expression
1
elscottab.1
⊢ x = y → φ ↔ ψ
2
scottss
⊢ Scott x | φ ⊆ x | φ
3
2
sseli
⊢ y ∈ Scott x | φ → y ∈ x | φ
4
vex
⊢ y ∈ V
5
4 1
elab
⊢ y ∈ x | φ ↔ ψ
6
3 5
sylib
⊢ y ∈ Scott x | φ → ψ