Description: A more general version of cbvrexf that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (Proof shortened by Mario Carneiro, 7-Dec-2014) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvralcsf.1 | ⊢ Ⅎ 𝑦 𝐴 | |
| cbvralcsf.2 | ⊢ Ⅎ 𝑥 𝐵 | ||
| cbvralcsf.3 | ⊢ Ⅎ 𝑦 𝜑 | ||
| cbvralcsf.4 | ⊢ Ⅎ 𝑥 𝜓 | ||
| cbvralcsf.5 | ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 ) | ||
| cbvralcsf.6 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | cbvrexcsf | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvralcsf.1 | ⊢ Ⅎ 𝑦 𝐴 | |
| 2 | cbvralcsf.2 | ⊢ Ⅎ 𝑥 𝐵 | |
| 3 | cbvralcsf.3 | ⊢ Ⅎ 𝑦 𝜑 | |
| 4 | cbvralcsf.4 | ⊢ Ⅎ 𝑥 𝜓 | |
| 5 | cbvralcsf.5 | ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 ) | |
| 6 | cbvralcsf.6 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 7 | 3 | nfn | ⊢ Ⅎ 𝑦 ¬ 𝜑 |
| 8 | 4 | nfn | ⊢ Ⅎ 𝑥 ¬ 𝜓 |
| 9 | 6 | notbid | ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
| 10 | 1 2 7 8 5 9 | cbvralcsf | ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) |
| 11 | 10 | notbii | ⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) |
| 12 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) | |
| 13 | dfrex2 | ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝜓 ) | |
| 14 | 11 12 13 | 3bitr4i | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜓 ) |