Description: Obsolete version of elopabr as of 11-Dec-2024. (Contributed by AV, 16-Feb-2021) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | elopabrOLD | ⊢ ( 𝐴 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 𝑅 𝑦 } → 𝐴 ∈ 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elopab | ⊢ ( 𝐴 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 𝑅 𝑦 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 𝑅 𝑦 ) ) | |
2 | df-br | ⊢ ( 𝑥 𝑅 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) | |
3 | 2 | biimpi | ⊢ ( 𝑥 𝑅 𝑦 → 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) |
4 | eleq1 | ⊢ ( 𝐴 = 〈 𝑥 , 𝑦 〉 → ( 𝐴 ∈ 𝑅 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) ) | |
5 | 3 4 | imbitrrid | ⊢ ( 𝐴 = 〈 𝑥 , 𝑦 〉 → ( 𝑥 𝑅 𝑦 → 𝐴 ∈ 𝑅 ) ) |
6 | 5 | imp | ⊢ ( ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 ) |
7 | 6 | exlimivv | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = 〈 𝑥 , 𝑦 〉 ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ∈ 𝑅 ) |
8 | 1 7 | sylbi | ⊢ ( 𝐴 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑥 𝑅 𝑦 } → 𝐴 ∈ 𝑅 ) |