Description: Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | dfse3 | ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) ∈ V ) |
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 ) |