Metamath Proof Explorer

Theorem riotaeqi

Description: Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypothesis riotaeqi.1 
|- A = B
Assertion riotaeqi 
|- ( iota_ x e. A ph ) = ( iota_ x e. B ph )

Proof

Step Hyp Ref Expression
1 riotaeqi.1 
 |-  A = B
2 biid 
 |-  ( ph <-> ph )
3 1 2 riotaeqbii 
 |-  ( iota_ x e. A ph ) = ( iota_ x e. B ph )