| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rabbidva2 | Structured version Visualization version GIF version | ||
| Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
| Ref | Expression |
|---|---|
| rabbidva2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
| Ref | Expression |
|---|---|
| rabbidva2 | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabbidva2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
| 2 | 1 | abbidv 2808 | . 2 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)}) |
| 3 | df-rab 3437 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
| 4 | df-rab 3437 | . 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)} | |
| 5 | 2, 3, 4 | 3eqtr4g 2802 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {cab 2714 {crab 3436 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-rab 3437 |
| This theorem is referenced by: rabbia2 3439 rabbidva 3443 rabeq 3451 rabeqbidva 3453 extmptsuppeq 8213 dfac2a 10170 hashbclem 14491 umgrislfupgrlem 29139 wwlksn0s 29881 wwlksnextwrd 29917 wpthswwlks2on 29981 rusgrnumwwlkl1 29988 clwwlknon1 30116 orvcgteel 34470 orvclteel 34475 wevgblacfn 35114 mapdvalc 41631 mapdval4N 41634 ovncvrrp 46579 ovnsubaddlem1 46585 ovnsubadd 46587 ovncvr2 46626 hspmbl 46644 smflim 46792 smflimsuplem1 46835 smflimsuplem3 46837 smflimsuplem7 46841 smflimsup 46843 |
| Copyright terms: Public domain | W3C validator |