Description: Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | coep.1 | ⊢ 𝐴 ∈ V | |
coep.2 | ⊢ 𝐵 ∈ V | ||
Assertion | coepr | ⊢ ( 𝐴 ( 𝑅 ∘ ◡ E ) 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coep.1 | ⊢ 𝐴 ∈ V | |
2 | coep.2 | ⊢ 𝐵 ∈ V | |
3 | vex | ⊢ 𝑥 ∈ V | |
4 | 1 3 | brcnv | ⊢ ( 𝐴 ◡ E 𝑥 ↔ 𝑥 E 𝐴 ) |
5 | 1 | epeli | ⊢ ( 𝑥 E 𝐴 ↔ 𝑥 ∈ 𝐴 ) |
6 | 4 5 | bitri | ⊢ ( 𝐴 ◡ E 𝑥 ↔ 𝑥 ∈ 𝐴 ) |
7 | 6 | anbi1i | ⊢ ( ( 𝐴 ◡ E 𝑥 ∧ 𝑥 𝑅 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) ) |
8 | 7 | exbii | ⊢ ( ∃ 𝑥 ( 𝐴 ◡ E 𝑥 ∧ 𝑥 𝑅 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) ) |
9 | 1 2 | brco | ⊢ ( 𝐴 ( 𝑅 ∘ ◡ E ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 ◡ E 𝑥 ∧ 𝑥 𝑅 𝐵 ) ) |
10 | df-rex | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) ) | |
11 | 8 9 10 | 3bitr4i | ⊢ ( 𝐴 ( 𝑅 ∘ ◡ E ) 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝐵 ) |