Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Class abstractions
bj-inrab
Next ⟩
bj-inrab2
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-inrab
Description:
Generalization of
inrab
.
(Contributed by
BJ
, 21-Apr-2019)
Ref
Expression
Assertion
bj-inrab
⊢
x
∈
A
|
φ
∩
x
∈
B
|
ψ
=
x
∈
A
∩
B
|
φ
∧
ψ
Proof
Step
Hyp
Ref
Expression
1
an4
⊢
x
∈
A
∧
φ
∧
x
∈
B
∧
ψ
↔
x
∈
A
∧
x
∈
B
∧
φ
∧
ψ
2
elin
⊢
x
∈
A
∩
B
↔
x
∈
A
∧
x
∈
B
3
2
anbi1i
⊢
x
∈
A
∩
B
∧
φ
∧
ψ
↔
x
∈
A
∧
x
∈
B
∧
φ
∧
ψ
4
1
3
bitr4i
⊢
x
∈
A
∧
φ
∧
x
∈
B
∧
ψ
↔
x
∈
A
∩
B
∧
φ
∧
ψ
5
4
abbii
⊢
x
|
x
∈
A
∧
φ
∧
x
∈
B
∧
ψ
=
x
|
x
∈
A
∩
B
∧
φ
∧
ψ
6
df-rab
⊢
x
∈
A
|
φ
=
x
|
x
∈
A
∧
φ
7
df-rab
⊢
x
∈
B
|
ψ
=
x
|
x
∈
B
∧
ψ
8
6
7
ineq12i
⊢
x
∈
A
|
φ
∩
x
∈
B
|
ψ
=
x
|
x
∈
A
∧
φ
∩
x
|
x
∈
B
∧
ψ
9
inab
⊢
x
|
x
∈
A
∧
φ
∩
x
|
x
∈
B
∧
ψ
=
x
|
x
∈
A
∧
φ
∧
x
∈
B
∧
ψ
10
8
9
eqtri
⊢
x
∈
A
|
φ
∩
x
∈
B
|
ψ
=
x
|
x
∈
A
∧
φ
∧
x
∈
B
∧
ψ
11
df-rab
⊢
x
∈
A
∩
B
|
φ
∧
ψ
=
x
|
x
∈
A
∩
B
∧
φ
∧
ψ
12
5
10
11
3eqtr4i
⊢
x
∈
A
|
φ
∩
x
∈
B
|
ψ
=
x
∈
A
∩
B
|
φ
∧
ψ