Theorem vtoclbg 3399

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 334	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3398	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1624   ∈ wcel 2131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-12 2188  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-v 3334

This theorem is referenced by:  alexeqg  3463  pm13.183  3476  sbc8g  3576  sbc2or  3577  sbcco  3591  sbc5  3593  sbcie2g  3602  eqsbc3  3608  sbcng  3609  sbcimg  3610  sbcan  3611  sbcor  3612  sbcbig  3613  sbcal  3618  sbcex2  3619  sbcel1v  3628  sbcreu  3648  csbiebg  3689  sbcel12  4118  sbceqg  4119  elpwg  4302  snssgOLD  4453  preq12bg  4522  elintgOLD  4628  elintrabg  4633  sbcbr123  4850  opelresgOLD  5555  inisegn0  5647  funfvima3  6650  elixpsn  8105  ixpsnf1o  8106  domeng  8127  1sdom  8320  rankcf  9783  eldm3  31950  br1steqgOLD  31971  br2ndeqgOLD  31972  elima4  31976  brsset  32294  brbigcup  32303  elfix2  32309  elfunsg  32321  elsingles  32323  funpartlem  32347  ellines  32557  elhf2g  32581  cover2g  33814  sbcrexgOLD  37843  sbcangOLD  39233  sbcorgOLD  39234  sbcalgOLD  39246  sbcexgOLD  39247  sbcel12gOLD  39248  sbcel1gvOLD  39585