Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
The Predecessor Class
elpredg
Next ⟩
predasetex
Metamath Proof Explorer
Ascii
Unicode
Theorem
elpredg
Description:
Membership in a predecessor class.
(Contributed by
Scott Fenton
, 17-Apr-2011)
Ref
Expression
Assertion
elpredg
⊢
X
∈
B
∧
Y
∈
A
→
Y
∈
Pred
R
A
X
↔
Y
R
X
Proof
Step
Hyp
Ref
Expression
1
df-pred
⊢
Pred
R
A
X
=
A
∩
R
-1
X
2
1
elin2
⊢
Y
∈
Pred
R
A
X
↔
Y
∈
A
∧
Y
∈
R
-1
X
3
2
baib
⊢
Y
∈
A
→
Y
∈
Pred
R
A
X
↔
Y
∈
R
-1
X
4
3
adantl
⊢
X
∈
B
∧
Y
∈
A
→
Y
∈
Pred
R
A
X
↔
Y
∈
R
-1
X
5
elimasng
⊢
X
∈
B
∧
Y
∈
A
→
Y
∈
R
-1
X
↔
X
Y
∈
R
-1
6
df-br
⊢
X
R
-1
Y
↔
X
Y
∈
R
-1
7
5
6
bitr4di
⊢
X
∈
B
∧
Y
∈
A
→
Y
∈
R
-1
X
↔
X
R
-1
Y
8
brcnvg
⊢
X
∈
B
∧
Y
∈
A
→
X
R
-1
Y
↔
Y
R
X
9
4
7
8
3bitrd
⊢
X
∈
B
∧
Y
∈
A
→
Y
∈
Pred
R
A
X
↔
Y
R
X