Description: Implicit substitution inference for ordered pairs. Compare copsex2g . (Contributed by NM, 26-Feb-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | copsex2ga.1 | ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | copsex2ga | ⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | copsex2ga.1 | ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | xpss | ⊢ ( 𝑉 × 𝑊 ) ⊆ ( V × V ) | |
| 3 | 2 | sseli | ⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → 𝐴 ∈ ( V × V ) ) |
| 4 | 1 | copsex2gb | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) ) |
| 5 | 4 | baibr | ⊢ ( 𝐴 ∈ ( V × V ) → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ) |
| 6 | 3 5 | syl | ⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ) |