| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > vtoclbg | Structured version Visualization version GIF version | ||
| Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
| Ref | Expression |
|---|---|
| vtoclbg.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
| vtoclbg.2 | ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) |
| vtoclbg.3 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| vtoclbg | ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vtoclbg.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 2 | vtoclbg.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) | |
| 3 | 1, 2 | bibi12d 348 | . 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃))) |
| 4 | vtoclbg.3 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
| 5 | 3, 4 | vtoclg 3521 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 = wceq 1569 ∈ wcel 2142 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 |
| This proof depends on definitions: df-bi 210 df-an 401 df-tru 1572 df-ex 1809 df-sb 2096 df-clab 2741 df-clel 2837 |
| This theorem is used by: alexeqg 3609 pm13.183 3624 elab6g 3627 elabgw 3635 sbc8g 3751 sbc2or 3752 sbccow 3766 sbcco 3769 sbc5ALT 3772 sbcie2g 3783 eqsbc1 3789 sbcng 3790 sbcimg 3791 sbcan 3792 sbcor 3793 sbcbig 3794 sbcal 3802 sbcex2 3803 sbcel1v 3808 sbcreu 3828 csbiebg 3884 sbcel12 4375 sbceqg 4376 csbie2df 4407 preq12bg 4817 elintrabg 4925 sbcbr123 5164 inisegn0 6099 fsn2g 7134 funfvima3 7234 elixpsn 8933 ixpsnf1o 8934 domeng 8957 rankcf 10768 kardeng 35578 eldm3 36261 elima4 36276 brsset 36387 brbigcup 36396 elfix2 36402 elfunsg 36414 elsingles 36416 funpartlem 36442 ellines 36652 elhf2g 36676 bj-elpwgALT 37718 cover2g 38395 |
| Copyright terms: Public domain | W3C validator |