Metamath Proof Explorer

Theorem dfrn7

Description: The range is equal to the image of any class including the domain. (Contributed by BJ, 27-Sep-2026)

Ref Expression
Assertion dfrn7 
|- ( dom A C_ B -> ran A = ( A " B ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 opeldm 
 |-  ( <. x , y >. e. A -> x e. dom A )
4 ssel 
 |-  ( dom A C_ B -> ( x e. dom A -> x e. B ) )
5 3 4 syl5 
 |-  ( dom A C_ B -> ( <. x , y >. e. A -> x e. B ) )
6 5 pm4.71rd 
 |-  ( dom A C_ B -> ( <. x , y >. e. A <-> ( x e. B /\ <. x , y >. e. A ) ) )
7 6 exbidv 
 |-  ( dom A C_ B -> ( E. x <. x , y >. e. A <-> E. x ( x e. B /\ <. x , y >. e. A ) ) )
8 7 abbidv 
 |-  ( dom A C_ B -> { y | E. x <. x , y >. e. A } = { y | E. x ( x e. B /\ <. x , y >. e. A ) } )
9 dfrn3 
 |-  ran A = { y | E. x <. x , y >. e. A }
10 dfima3 
 |-  ( A " B ) = { y | E. x ( x e. B /\ <. x , y >. e. A ) }
11 8 9 10 3eqtr4g 
 |-  ( dom A C_ B -> ran A = ( A " B ) )