Description: Obsolete proof of cnvsym as of 29-Dec-2024. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by SN, 23-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvsymOLD | ⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relcnv | ⊢ Rel ◡ 𝑅 | |
| 2 | ssrel3 | ⊢ ( Rel ◡ 𝑅 → ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ) ) | |
| 3 | 1 2 | ax-mp | ⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ) |
| 4 | alcom | ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ) | |
| 5 | vex | ⊢ 𝑦 ∈ V | |
| 6 | vex | ⊢ 𝑥 ∈ V | |
| 7 | 5 6 | brcnv | ⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) |
| 8 | 7 | imbi1i | ⊢ ( ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |
| 9 | 8 | 2albii | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 ◡ 𝑅 𝑥 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |
| 10 | 3 4 9 | 3bitri | ⊢ ( ◡ 𝑅 ⊆ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ) |