Metamath Proof Explorer


Theorem dfse3

Description: Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion dfse3 ( 𝑅 Se 𝐴 ↔ ∀ 𝑥𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) ∈ V )

Proof

Step Hyp Ref Expression
1 dfse2 ( 𝑅 Se 𝐴 ↔ ∀ 𝑥𝐴 ( 𝐴 ∩ ( 𝑅 “ { 𝑥 } ) ) ∈ V )
2 df-pred Pred ( 𝑅 , 𝐴 , 𝑥 ) = ( 𝐴 ∩ ( 𝑅 “ { 𝑥 } ) )
3 2 eleq1i ( Pred ( 𝑅 , 𝐴 , 𝑥 ) ∈ V ↔ ( 𝐴 ∩ ( 𝑅 “ { 𝑥 } ) ) ∈ V )
4 3 ralbii ( ∀ 𝑥𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) ∈ V ↔ ∀ 𝑥𝐴 ( 𝐴 ∩ ( 𝑅 “ { 𝑥 } ) ) ∈ V )
5 1 4 bitr4i ( 𝑅 Se 𝐴 ↔ ∀ 𝑥𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) ∈ V )