Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Misc. Useful Theorems
riotarab
Next ⟩
reurab
Metamath Proof Explorer
Ascii
Unicode
Theorem
riotarab
Description:
Restricted iota of a restricted abstraction.
(Contributed by
Scott Fenton
, 8-Aug-2024)
Ref
Expression
Hypothesis
riotarab.1
⊢
x
=
y
→
φ
↔
ψ
Assertion
riotarab
⊢
ι
x
∈
y
∈
A
|
ψ
|
χ
=
ι
x
∈
A
|
φ
∧
χ
Proof
Step
Hyp
Ref
Expression
1
riotarab.1
⊢
x
=
y
→
φ
↔
ψ
2
1
bicomd
⊢
x
=
y
→
ψ
↔
φ
3
2
equcoms
⊢
y
=
x
→
ψ
↔
φ
4
3
elrab
⊢
x
∈
y
∈
A
|
ψ
↔
x
∈
A
∧
φ
5
4
anbi1i
⊢
x
∈
y
∈
A
|
ψ
∧
χ
↔
x
∈
A
∧
φ
∧
χ
6
anass
⊢
x
∈
A
∧
φ
∧
χ
↔
x
∈
A
∧
φ
∧
χ
7
5
6
bitri
⊢
x
∈
y
∈
A
|
ψ
∧
χ
↔
x
∈
A
∧
φ
∧
χ
8
7
iotabii
⊢
ι
x
|
x
∈
y
∈
A
|
ψ
∧
χ
=
ι
x
|
x
∈
A
∧
φ
∧
χ
9
df-riota
⊢
ι
x
∈
y
∈
A
|
ψ
|
χ
=
ι
x
|
x
∈
y
∈
A
|
ψ
∧
χ
10
df-riota
⊢
ι
x
∈
A
|
φ
∧
χ
=
ι
x
|
x
∈
A
∧
φ
∧
χ
11
8
9
10
3eqtr4i
⊢
ι
x
∈
y
∈
A
|
ψ
|
χ
=
ι
x
∈
A
|
φ
∧
χ